ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_4<GOAL>Nat.card α = if h : Finite α then Fintype.card α else 0
<VAR>α : Type u_1<VAR>Finite α<GOAL>0 < Nat.card α ↔ Nonempty α
<VAR>α : Type u_1<VAR>Finite α<VAR>h : Nonempty α<GOAL>0 < Nat.card α
<VAR>α : Type u_4<VAR>Finite α<GOAL>↑(Nat.card α) = Cardinal.mk α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>Finite β<GOAL>Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
<VAR>α : Type u_1<VAR>Finite α<GOAL>Nat.card α ≤ 1 ↔ Subsingleton α
<VAR>α : Type u_1<VAR>Finite α<GOAL>1 < Nat.card α ↔ Nontrivial α
<VAR>α : Type u_1<VAR>Finite α<VAR>h : Nontrivial α<GOAL>1 < Nat.card α
<VAR>α : Type u_1<VAR>Finite α<GOAL>Nat.card (Option α) = Nat.card α + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>f : α ↪ β<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Nat.card β ≤ Nat.card α
<VAR>α : Type u_1<VAR>Finite α<GOAL>Nat.card α = 0 ↔ IsEmpty α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>h : Nat.card β = 0 → Nat.card α = 0<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>h : Nat.card β = 0 → Nat.card α = 0<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : Nat.card α = 0 → Nat.card β = 0<GOAL>Nat.card β ≤ Nat.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : Nat.card β = 0<GOAL>Nat.card α = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>h : Nat.card α = 0<GOAL>Nat.card β = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α ↪ β<VAR>h : Nat.card α = 0<GOAL>Nat.card β = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>Finite ↑s<VAR>f : α → β<GOAL>Nat.card ↑(f '' s) ≤ Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>f : α → β<GOAL>Nat.card ↑(Set.range f) ≤ Nat.card α
<VAR>α : Type u_1<VAR>Finite α<VAR>p : α → Prop<GOAL>Nat.card { x // p x } ≤ Nat.card α
<VAR>α : Type u_1<VAR>Finite α<VAR>p : α → Prop<VAR>x : α<VAR>hx : ¬p x<GOAL>Nat.card { x // p x } < Nat.card α
<VAR>α : Type u_4<VAR>Finite α<GOAL>PartENat.card α = ↑(Nat.card α)
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hsub : s ⊂ t<GOAL>Nat.card ↑s < Nat.card ↑t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite<VAR>hsub : s ⊆ t<VAR>hcard : Nat.card ↑t ≤ Nat.card ↑s<GOAL>s = t
<VAR>α : Type u_1<VAR>s : Set α<VAR>e : α ≃ α<VAR>hs : s.Finite<GOAL>⇑e '' s = s ↔ ⇑e '' s ⊆ s
<GOAL>List.Nat.antidiagonalTuple 0 0 = [![]]
<VAR>n : ℕ<GOAL>List.Nat.antidiagonalTuple 0 (n + 1) = []
<VAR>n k : ℕ<VAR>x : Fin k → ℕ<GOAL>x ∈ List.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
<VAR>k n : ℕ<GOAL>(List.Nat.antidiagonalTuple k n).Nodup
<VAR>k : ℕ<GOAL>List.Nat.antidiagonalTuple k 0 = [0]
<VAR>n : ℕ<GOAL>List.Nat.antidiagonalTuple 1 n = [![n]]
<VAR>n : ℕ<GOAL>List.Nat.antidiagonalTuple 2 n = List.map (fun i => ![i.1, i.2]) (List.Nat.antidiagonal n)
<VAR>k n : ℕ<GOAL>List.Pairwise (Pi.Lex (fun x x_1 => x < x_1) fun x x x_1 => x < x_1) (List.Nat.antidiagonalTuple k n)
<GOAL>Multiset.Nat.antidiagonalTuple 0 0 = {![]}
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonalTuple 0 n.succ = 0
<VAR>n k : ℕ<VAR>x : Fin k → ℕ<GOAL>x ∈ Multiset.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
<VAR>k n : ℕ<GOAL>(Multiset.Nat.antidiagonalTuple k n).Nodup
<VAR>k : ℕ<GOAL>Multiset.Nat.antidiagonalTuple k 0 = {0}
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonalTuple 1 n = {![n]}
<VAR>n : ℕ<GOAL>Multiset.Nat.antidiagonalTuple 2 n = Multiset.map (fun i => ![i.1, i.2]) (Multiset.Nat.antidiagonal n)
<GOAL>Finset.Nat.antidiagonalTuple 0 0 = {![]}
<VAR>n : ℕ<GOAL>Finset.Nat.antidiagonalTuple 0 n.succ = ∅
<VAR>n k : ℕ<VAR>x : Fin k → ℕ<GOAL>x ∈ Finset.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
<VAR>k : ℕ<GOAL>Finset.Nat.antidiagonalTuple k 0 = {0}
<VAR>n : ℕ<GOAL>Finset.Nat.antidiagonalTuple 1 n = {![n]}
<VAR>n : ℕ<GOAL>Finset.Nat.antidiagonalTuple 2 n = Finset.map (piFinTwoEquiv fun x => ℕ).symm.toEmbedding (Finset.antidiagonal n)
<VAR>k : ℕ<VAR>x : Fin k → ℕ<GOAL>∀ (a : Fin k), ↑((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).snd a = x a
<VAR>k : ℕ<VAR>x : (n : ℕ) × { x // x ∈ Finset.Nat.antidiagonalTuple k n }<GOAL>∀ (a : Fin k), (Finset.Nat.sigmaAntidiagonalTupleEquivTuple k) x a = ↑x.snd a
<VAR>k : ℕ<VAR>x : Fin k → ℕ<GOAL>((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).fst = ∑ i : Fin k, x i
<VAR>n : ℕ<GOAL>Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n
<VAR>n a b : ℕ<VAR>H : Nat.unpair n = (a, b)<GOAL>Nat.pair a b = n
<VAR>a b : ℕ<GOAL>Nat.unpair (Nat.pair a b) = (a, b)
<GOAL>⇑Nat.pairEquiv.symm = Nat.unpair
<GOAL>⇑Nat.pairEquiv = Function.uncurry Nat.pair
<VAR>a b c d : ℕ<GOAL>Nat.pair a b = Nat.pair c d ↔ a = c ∧ b = d
<VAR>n : ℕ<VAR>n1 : 1 ≤ n<GOAL>(Nat.unpair n).1 < n
<VAR>n : ℕ<GOAL>(Nat.unpair n).1 ≤ n
<VAR>a b : ℕ<GOAL>a ≤ Nat.pair a b
<VAR>a b : ℕ<GOAL>b ≤ Nat.pair a b
<VAR>n : ℕ<GOAL>(Nat.unpair n).2 ≤ n
<VAR>a₁ a₂ : ℕ<VAR>b : ℕ<VAR>h : a₁ < a₂<GOAL>Nat.pair a₁ b < Nat.pair a₂ b
<VAR>a : ℕ<VAR>b₁ b₂ : ℕ<VAR>h : b₁ < b₂<GOAL>Nat.pair a b₁ < Nat.pair a b₂
<VAR>m n : ℕ<GOAL>Nat.pair m n < (max m n + 1) ^ 2
<VAR>m n : ℕ<GOAL>max m n ^ 2 + min m n ≤ Nat.pair m n
<VAR>m n : ℕ<GOAL>m + n ≤ Nat.pair m n
<VAR>n : ℕ<GOAL>(Nat.unpair n).1 + (Nat.unpair n).2 ≤ n
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → ℕ → α<GOAL>⨆ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨆ i, ⨆ j, f i j
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℕ → ℕ → α<GOAL>⨅ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨅ i, ⨅ j, f i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : ℕ → Set α<VAR>t : ℕ → Set β<GOAL>⋃ n, s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n
<VAR>α : Type u_1<VAR>f : ℕ → ℕ → Set α<GOAL>⋃ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋃ i, ⋃ j, f i j
<VAR>α : Type u_1<VAR>f : ℕ → ℕ → Set α<GOAL>⋂ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋂ i, ⋂ j, f i j
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>n : ℕ<GOAL>(↑n)⁻¹ ≤ 1
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>m n : ℕ<GOAL>↑(m / n) ≤ ↑m / ↑n
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>n : ℕ<GOAL>0 < (↑n + 1)⁻¹
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>n : ℕ<GOAL>0 < 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n ≤ m<GOAL>1 / (↑m + 1) ≤ 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>LinearOrderedSemifield α<VAR>n m : ℕ<VAR>h : n < m<GOAL>1 / (↑m + 1) < 1 / (↑n + 1)
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<GOAL>Monotone Nat.cast
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>a b : ℕ<VAR>h : a ≤ b<GOAL>↑a ≤ ↑b
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>n : ℕ<GOAL>0 ≤ ↑n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>0 ≤ OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>n : ℕ<GOAL>0 < ↑n + 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>n : ℕ<GOAL>0 < ↑n ↔ 0 < n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<GOAL>StrictMono Nat.cast
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<GOAL>⇑Nat.castOrderEmbedding = Nat.cast
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<GOAL>↑m < ↑n ↔ m < n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<GOAL>1 < ↑n ↔ 1 < n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<GOAL>1 ≤ ↑n ↔ 1 ≤ n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<GOAL>↑n < 1 ↔ n = 0
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<GOAL>↑n ≤ 1 ↔ n ≤ 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>m.AtLeastTwo<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>m.AtLeastTwo<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>m.AtLeastTwo<GOAL>OfNat.ofNat m ≤ ↑n ↔ OfNat.ofNat m ≤ n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>m.AtLeastTwo<GOAL>OfNat.ofNat m < ↑n ↔ OfNat.ofNat m < n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>n.AtLeastTwo<GOAL>↑m ≤ OfNat.ofNat n ↔ m ≤ OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>m n : ℕ<VAR>n.AtLeastTwo<GOAL>↑m < OfNat.ofNat n ↔ m < OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>1 < OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>1 ≤ OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>¬OfNat.ofNat n ≤ 1
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>CharZero α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>¬OfNat.ofNat n < 1
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>FunLike F R S<VAR>n : ℕ<VAR>h : NeZero ↑n<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>NeZero ↑n
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>m n : ℕ<VAR>n_dvd : n ∣ m<VAR>hn : ↑n ≠ 0<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>CharZero α<VAR>m n d : ℕ<VAR>hn : d ∣ n<VAR>hm : d ∣ m<GOAL>↑(m / d) / ↑(n / d) = ↑m / ↑n
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: β)<VAR>x : β<GOAL>MvPFunctor.M.dest (MvQPF.P F) (MvQPF.corecF g x) = (TypeVec.id ::: MvQPF.corecF g) <$$> MvQPF.repr (g x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: β)<VAR>x : β<GOAL>(MvQPF.Cofix.corec g x).dest = (TypeVec.id ::: MvQPF.Cofix.corec g) <$$> g x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop<VAR>h' : ∀ (x : MvQPF.Cofix F α), r x x<VAR>h : ∀ (x y : MvQPF.Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>x y : MvQPF.Cofix F α<GOAL>r x y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop<VAR>h : ∀ (x y : MvQPF.Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>x y : MvQPF.Cofix F α<GOAL>r x y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop<VAR>h : ∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR (fun {i} => α.RelLast r) x.dest y.dest<VAR>x y : MvQPF.Cofix F α<GOAL>r x y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop<VAR>h : ∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR' (α.RelLast' r) x.dest y.dest<VAR>x y : MvQPF.Cofix F α<GOAL>r x y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u_1<VAR>Q : β → Prop<VAR>u v : β → MvQPF.Cofix F α<VAR>h : ∀ (x : β), Q x → ∃ a f' f₀ f₁, (u x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₀⟩ ∧ (v x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₁⟩ ∧ ∀ (i : (MvQPF.P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'<VAR>x : β<GOAL>Q x → u x = v x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : MvQPF.Cofix F α<GOAL>MvQPF.Cofix.mk x.dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: MvQPF.Cofix F α)<GOAL>(MvQPF.Cofix.mk x).dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : MvQPF.Cofix F α<VAR>h : x.dest = y.dest<GOAL>x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : F (α ::: MvQPF.Cofix F α)<VAR>h : MvQPF.Cofix.mk x = MvQPF.Cofix.mk y<GOAL>x = y
<VAR>n : ℕ<VAR>α β : TypeVec.{u_1} n<VAR>F' : TypeVec.{u_1} n → Type u<VAR>MvFunctor F'<VAR>LawfulMvFunctor F'<VAR>R : β ⊗ β ⟹ TypeVec.repeat n Prop<VAR>x : F' α<VAR>f g : α ⟹ β<VAR>h : α ⟹ TypeVec.Subtype_ R<VAR>hh : TypeVec.subtypeVal R ⊚ h = (f ⊗' g) ⊚ TypeVec.prod.diag<GOAL>MvFunctor.LiftR' R (f <$$> x) (g <$$> x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>lawful : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι ι' : Type u<VAR>R : ι' → ι' → Prop<VAR>x : F (α ::: ι)<VAR>f g : ι → ι'<VAR>hh : ∀ (x : ι), R (f x) (g x)<GOAL>MvFunctor.LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: g) <$$> x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι : Type u<VAR>R : ι → ι → Prop<VAR>x : F (α ::: ι)<VAR>f : ι → ι<VAR>hh : ∀ (x : ι), R (f x) x<GOAL>MvFunctor.LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : MvQPF.Cofix F α<GOAL>Quot.mk MvQPF.Mcongr x.repr = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<GOAL>MvQPF.Cofix.corec (g ∘ f) x₀ = MvQPF.Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))<VAR>x : β<GOAL>(MvQPF.Cofix.corec' g x).dest = (TypeVec.id ::: Sum.elim id (MvQPF.Cofix.corec' g)) <$$> g x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : {X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)<VAR>x : β<VAR>h : ∀ (X Y : Type u) (f : MvQPF.Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x<GOAL>(MvQPF.Cofix.corec₁ g x).dest = g id (MvQPF.Cofix.corec₁ g) x
<VAR>n : ℕ<GOAL>↑n = ↑n
<VAR>α : Type u_3<VAR>OrderedSemiring α<VAR>n : ℕ<GOAL>0 ≤ ↑n
<VAR>α : Type u_3<VAR>OrderedSemiring α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>0 ≤ OfNat.ofNat n
<VAR>α : Type u_3<VAR>LinearOrderedSemiring α<VAR>a b : ℕ<GOAL>↑(min a b) = min ↑a ↑b
<VAR>α : Type u_3<VAR>LinearOrderedSemiring α<VAR>a b : ℕ<GOAL>↑(max a b) = max ↑a ↑b
<VAR>α : Type u_3<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>n : ℕ<GOAL>0 < ↑n ↔ 0 < n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>PartialOrder α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>ZeroLEOneClass α<VAR>NeZero 1<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>0 < OfNat.ofNat n
<VAR>α : Type u_3<VAR>OrderedSemiring α<VAR>Nontrivial α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>0 < OfNat.ofNat n
<VAR>α : Type u_1<VAR>CanonicallyOrderedCommSemiring α<VAR>Sub α<VAR>OrderedSub α<VAR>ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>m n : ℕ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>a : ℕ<GOAL>|↑a| = ↑a
<VAR>α : Type u_1<VAR>LinearOrderedRing α<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>|OfNat.ofNat n| = OfNat.ofNat n
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<GOAL>⇑(Nat.castAddMonoidHom α) = Nat.cast
<VAR>α : Type u_1<VAR>AddMonoidWithOne α<VAR>n : ℕ<VAR>hn : Even n<GOAL>Even ↑n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>m n : ℕ<GOAL>↑(m * n) = ↑m * ↑n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<GOAL>⇑(Nat.castRingHom α) = Nat.cast
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>n • a = a * ↑n
<VAR>α : Type u_1<VAR>NonAssocSemiring α<VAR>n : ℕ<VAR>a : α<GOAL>n • a = ↑n * a
<VAR>α : Type u_1<VAR>Semiring α<VAR>m n : ℕ<GOAL>↑(m ^ n) = ↑m ^ n
<VAR>α : Type u_1<VAR>Semiring α<VAR>m n : ℕ<VAR>h : m ∣ n<GOAL>↑m ∣ ↑n
<VAR>A : Type u_3<VAR>F : Type u_5<VAR>FunLike F ℕ A<VAR>AddMonoid A<VAR>AddMonoidHomClass F ℕ A<VAR>f g : F<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>A : Type u_3<VAR>AddMonoid A<VAR>f g : ℕ →+ A<GOAL>f 1 = g 1 → f = g
<VAR>A : Type u_3<VAR>F : Type u_5<VAR>FunLike F ℕ A<VAR>AddMonoidWithOne A<VAR>AddMonoidHomClass F ℕ A<VAR>f : F<VAR>h1 : f 1 = 1<VAR>n : ℕ<GOAL>f n = ↑n
<VAR>B : Type u_4<VAR>F : Type u_5<VAR>AddMonoidWithOne B<VAR>A : Type u_6<VAR>AddMonoidWithOne A<VAR>FunLike F A B<VAR>AddMonoidHomClass F A B<VAR>f : F<VAR>h : f 1 = 1<VAR>n : ℕ<GOAL>f ↑n = ↑n
<VAR>B : Type u_4<VAR>F : Type u_5<VAR>AddMonoidWithOne B<VAR>A : Type u_6<VAR>AddMonoidWithOne A<VAR>FunLike F A B<VAR>AddMonoidHomClass F A B<VAR>f : F<VAR>h : f 1 = 1<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (OfNat.ofNat n) = OfNat.ofNat n
<VAR>A : Type u_6<VAR>AddMonoidWithOne A<VAR>n : ℕ<GOAL>n • 1 = ↑n
<VAR>A : Type u_3<VAR>F : Type u_4<VAR>MulZeroOneClass A<VAR>FunLike F ℕ A<VAR>MonoidWithZeroHomClass F ℕ A<VAR>f g : F<VAR>h_pos : ∀ {n : ℕ}, 0 < n → f n = g n<GOAL>f = g
<VAR>A : Type u_3<VAR>MulZeroOneClass A<VAR>f g : ℕ →*₀ A<GOAL>(∀ {n : ℕ}, 0 < n → f n = g n) → f = g
<VAR>R : Type u_3<VAR>F : Type u_5<VAR>NonAssocSemiring R<VAR>FunLike F ℕ R<VAR>RingHomClass F ℕ R<VAR>f : F<VAR>n : ℕ<GOAL>f n = ↑n
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>n : ℕ<GOAL>f ↑n = ↑n
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>f (OfNat.ofNat n) = OfNat.ofNat n
<VAR>R : Type u_3<VAR>F : Type u_5<VAR>NonAssocSemiring R<VAR>FunLike F ℕ R<VAR>RingHomClass F ℕ R<VAR>f g : F<GOAL>f = g
<VAR>R : Type u_6<VAR>S : Type u_7<VAR>Semiring R<VAR>Semiring S<VAR>F : Type u_8<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>n : ℕ<VAR>hn : NeZero ↑n<GOAL>NeZero ↑n
<VAR>R : Type u_3<VAR>NonAssocSemiring R<VAR>f : ℕ →+* R<GOAL>f = Nat.castRingHom R
<GOAL>Nat.castRingHom ℕ = RingHom.id ℕ
<VAR>β : Type u_2<VAR>AddMonoid β<VAR>x : β<VAR>n : ℕ<GOAL>((multiplesHom β) x) n = n • x
<VAR>α : Type u_1<VAR>Monoid α<VAR>x : α<VAR>n : Multiplicative ℕ<GOAL>((powersHom α) x) n = x ^ Multiplicative.toAdd n
<VAR>β : Type u_2<VAR>AddMonoid β<VAR>f : ℕ →+ β<GOAL>(multiplesHom β).symm f = f 1
<VAR>α : Type u_1<VAR>Monoid α<VAR>f : Multiplicative ℕ →* α<GOAL>(powersHom α).symm f = f (Multiplicative.ofAdd 1)
<VAR>α : Type u_1<VAR>Monoid α<VAR>f : Multiplicative ℕ →* α<VAR>n : Multiplicative ℕ<GOAL>f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n
<VAR>α : Type u_1<VAR>Monoid α<VAR>f g : Multiplicative ℕ →* α<VAR>h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)<GOAL>f = g
<VAR>β : Type u_2<VAR>AddMonoid β<VAR>f : ℕ →+ β<VAR>n : ℕ<GOAL>f n = n • f 1
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>x : β<VAR>n : ℕ<GOAL>((multiplesAddHom β) x) n = n • x
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>x : α<VAR>n : Multiplicative ℕ<GOAL>((powersMulHom α) x) n = x ^ Multiplicative.toAdd n
<VAR>β : Type u_2<VAR>AddCommMonoid β<VAR>f : ℕ →+ β<GOAL>(multiplesAddHom β).symm f = f 1
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>f : Multiplicative ℕ →* α<GOAL>(powersMulHom α).symm f = f (Multiplicative.ofAdd 1)
<VAR>α : Type u_1<VAR>π : α → Type u_3<VAR>(a : α) → NatCast (π a)<VAR>n : ℕ<VAR>a : α<GOAL>↑n a = ↑n
<VAR>α : Type u_1<VAR>π : α → Type u_3<VAR>(a : α) → NatCast (π a)<VAR>n : ℕ<GOAL>↑n = fun x => ↑n
<VAR>α : Type u_1<VAR>π : α → Type u_3<VAR>(a : α) → NatCast (π a)<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>a : α<GOAL>OfNat.ofNat n a = ↑n
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>NatCast γ<VAR>n : ℕ<GOAL>Sum.elim ↑n ↑n = ↑n
<VAR>b n : ℕ<GOAL>Nat.log b n = 0 ↔ n < b ∨ b ≤ 1
<VAR>b n : ℕ<VAR>hb : n < b<GOAL>Nat.log b n = 0
<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>n : ℕ<GOAL>Nat.log b n = 0
<VAR>b n : ℕ<GOAL>0 < Nat.log b n ↔ b ≤ n ∧ 1 < b
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hbn : b ≤ n<GOAL>0 < Nat.log b n
<VAR>b n : ℕ<VAR>h : 1 < b<VAR>hn : b ≤ n<GOAL>Nat.log b n = Nat.log b (n / b) + 1
<VAR>n : ℕ<GOAL>Nat.log 0 n = 0
<VAR>b : ℕ<GOAL>Nat.log b 0 = 0
<VAR>n : ℕ<GOAL>Nat.log 1 n = 0
<VAR>b : ℕ<GOAL>Nat.log b 1 = 0
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x y : ℕ<VAR>hy : y ≠ 0<GOAL>b ^ x ≤ y ↔ x ≤ Nat.log b y
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x y : ℕ<VAR>hy : y ≠ 0<GOAL>y < b ^ x ↔ Nat.log b y < x
<VAR>b x y : ℕ<VAR>hy : y ≠ 0<VAR>h : x ≤ Nat.log b y<GOAL>b ^ x ≤ y
<VAR>b x y : ℕ<VAR>hb : 1 < b<VAR>h : b ^ x ≤ y<GOAL>x ≤ Nat.log b y
<VAR>b : ℕ<VAR>x : ℕ<VAR>hx : x ≠ 0<GOAL>b ^ Nat.log b x ≤ x
<VAR>b x y : ℕ<VAR>hy : y ≠ 0<GOAL>y < b ^ x → Nat.log b y < x
<VAR>b x y : ℕ<VAR>hb : 1 < b<GOAL>Nat.log b y < x → y < b ^ x
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<GOAL>x < b ^ (Nat.log b x).succ
<VAR>b m n : ℕ<VAR>h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0<GOAL>Nat.log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)
<VAR>b m n : ℕ<VAR>h₁ : b ^ m ≤ n<VAR>h₂ : n < b ^ (m + 1)<GOAL>Nat.log b n = m
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<GOAL>Nat.log b (b ^ x) = x
<VAR>b n : ℕ<GOAL>Nat.log b n = 1 ↔ b ≤ n ∧ n < b * b
<VAR>b n : ℕ<GOAL>Nat.log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b ≤ n
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>Nat.log b (n * b) = Nat.log b n + 1
<VAR>b x : ℕ<GOAL>b ^ Nat.log b x ≤ x + 1
<VAR>b : ℕ<GOAL>Monotone (Nat.log b)
<VAR>b n m : ℕ<VAR>h : n ≤ m<GOAL>Nat.log b n ≤ Nat.log b m
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>Nat.log b n ≤ Nat.log c n
<VAR>n : ℕ<GOAL>AntitoneOn (fun b => Nat.log b n) (Set.Ioi 1)
<VAR>b n : ℕ<GOAL>Nat.log b (n / b) = Nat.log b n - 1
<VAR>b n : ℕ<GOAL>Nat.log b (n / b * b) = Nat.log b n
<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>n : ℕ<GOAL>Nat.clog b n = 0
<VAR>n : ℕ<VAR>hn : n ≤ 1<VAR>b : ℕ<GOAL>Nat.clog b n = 0
<VAR>n : ℕ<GOAL>Nat.clog 0 n = 0
<VAR>b : ℕ<GOAL>Nat.clog b 0 = 0
<VAR>n : ℕ<GOAL>Nat.clog 1 n = 0
<VAR>b : ℕ<GOAL>Nat.clog b 1 = 0
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>Nat.clog b n = Nat.clog b ((n + b - 1) / b) + 1