mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_iff_exists_zpowers_eq_top : ∀ {α : Type u_1} [inst : Group α], IsCyclic α ↔ ∃ g, Subgroup.zpowers g = ⊤
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `leftComm` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.rightComm_eq : ∀ (R : Type uR) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q] [inst_5 : Module R Q]
  [inst_6 : Module R P], TensorProduct.AlgebraTensorModule.rightComm R R R M P Q = TensorProduct.rightComm R M P Q
-- Init.Data.Int.Order
Int.toNat_add_toNat_neg_eq_natAbs : ∀ (n : ℤ), n.toNat + (-n).toNat = n.natAbs
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.append_nil : ∀ {α : Type u} (s : Stream'.WSeq α), s.append Stream'.WSeq.nil = s
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getDₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a), m.getDₘ a fallback = (m.get?ₘ a).getD fallback
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.le_normalizer_iff_addCommutator_le_left : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ AddSubgroup.normalizer ↑K ↔ ⁅K, H⁆ ≤ K
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.DTreeMap.Raw.Const.mergeWith : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      (α → β → β → β) →
        Std.DTreeMap.Raw α (fun x => β) cmp → Std.DTreeMap.Raw α (fun x => β) cmp → Std.DTreeMap.Raw α (fun x => β) cmp
-- Mathlib.Geometry.Manifold.PoincareConjecture
/-- The smooth Poincaré conjecture; true for n = 1, 2, 3, 5, 6, 12, 56, and 61,
open for n = 4, and it is conjectured that there are no other n > 4 for which it is true
(Conjecture 1.17, https://annals.math.princeton.edu/2017/186-2/p03).  -/
ContinuousMap.HomotopyEquiv.NonemptyDiffeomorphSphere : (M : Type u_1) → [TopologicalSpace M] → ℕ → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X Z) f
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.decidableMemMultiples.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M},
  AddSubmonoid.decidableMemMultiples = Classical.decPred fun x => x ∈ AddSubmonoid.multiples a
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/(ker φ) ≃+ H` induced by a
homomorphism `φ : G →+ H` with a right inverse `ψ : H → G`.  -/
QuotientAddGroup.quotientKerEquivOfRightInverse : {G : Type u} →
  [inst : AddGroup G] →
    {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → (ψ : H → G) → Function.RightInverse ψ ⇑φ → G ⧸ φ.ker ≃+ H
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.sSup_ord : ∀ (s : Set Cardinal.{u_3}), (sSup s).ord = sSup (Cardinal.ord '' s)
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl.congr_simp : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) (φ φ_1 : ↥p →ₗ[R] F),
  φ = φ_1 → ∀ (ψ ψ_1 : ↥q →ₗ[R] F), ψ = ψ_1 → LinearMap.ofIsCompl h φ ψ = LinearMap.ofIsCompl h φ_1 ψ_1
-- Mathlib.Data.Finset.Sups
Finset.compls_singleton : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), {a}.compls = {aᶜ}
-- Mathlib.Data.Part
Part.eq_some_iff : ∀ {α : Type u_1} {a : α} {o : Part α}, o = Part.some a ↔ a ∈ o
-- Mathlib.Algebra.CharP.CharAndCard
charP_of_card_eq_prime : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Fintype R] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Fintype.card R = p → CharP R p
-- Init.Data.Array.Extract
Array.takeWhile_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool},
  Array.takeWhile p (Array.replicate n a) = if p a = true then Array.replicate n a else #[]
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_iUnion_fintype_le : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Fintype β]
  (f : β → Set α), μ.real (⋃ b, f b) ≤ ∑ p, μ.real (f p)
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson.eq_1 : ∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (τ : UpperHalfPlane),
  UpperHalfPlane.petersson k f f' τ = (starRingEnd ℂ) (f τ) * f' τ * ↑τ.im ^ k
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNatLT : ∀ {n : ℕ} (h : n < UInt32.size), (UInt32.ofNatLT n h).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.min_edist_le_edist_pi : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → EDist (F i)] (x y : (i : ι) → F i) (i : ι),
  min (2⁻¹ ^ Encodable.encode i) (edist (x i) (y i)) ≤ edist x y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `f ∘ g = id` as `ContinuousLinearMap`s implies `f ∘ g = id` as functions.  -/
ContinuousLinearMap.rightInverse_of_comp : ∀ {R : Type u_9} {E : Type u_10} {F : Type u_11} [inst : Semiring R] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} {g : F →L[R] E},
  f ∘SL g = ContinuousLinearMap.id R F → Function.RightInverse ⇑g ⇑f
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodUnique_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Unique N] (a : M × N),
  MulEquiv.prodUnique a = a.1
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The cusp function of the discriminant equals `q * ∏' n, (1 - q^(n+1))^24`
on the open unit disc.  -/
ModularForm.discriminant_cuspFunction_eqOn : Set.EqOn (UpperHalfPlane.cuspFunction 1 ModularForm.discriminant) (fun q => q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24)
  (Metric.ball 0 1)
-- Mathlib.Data.Vector.Basic
List.Vector.get_set_same : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n) (a : α), (v.set i a).get i = a
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueRingEquiv_symm_apply : ∀ {m : Type u_1} {A : Type u_3} [inst : Unique m] [inst_1 : NonUnitalNonAssocSemiring A] (a : A),
  Matrix.uniqueRingEquiv.symm a = Matrix.of fun x x_1 => a
-- Init.Data.List.Control
List.filterMapM.loop : {m : Type u → Type v} → [Monad m] → {α : Type w} → {β : Type u} → (α → m (Option β)) → List α → List β → m (List β)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.withSeminorms : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F], WithSeminorms (ContinuousLinearMapWOT.seminormFamily σ E F)
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The constant sheaf functor commutes with `sheafCompose J U` up to isomorphism, provided that `U`
preserves sheafification.
 -/
CategoryTheory.constantCommuteCompose : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            {B : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_3, u_3} B] →
                (U : CategoryTheory.Functor D B) →
                  [inst_4 : CategoryTheory.HasWeakSheafify J B] →
                    [J.PreservesSheafification U] →
                      [inst_6 : J.HasSheafCompose U] →
                        (CategoryTheory.constantSheaf J D).comp (CategoryTheory.sheafCompose J U) ≅
                          U.comp (CategoryTheory.constantSheaf J B)
-- Init.Data.String.Basic
String.Slice.Pos.ofStr.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.str.Pos) (e_pos : pos = pos_1) (h₁ : s.startInclusive ≤ pos)
  (h₂ : pos ≤ s.endExclusive), String.Slice.Pos.ofStr pos h₁ h₂ = String.Slice.Pos.ofStr pos_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  a ≤ b → CategoryTheory.IsIso (t.eTruncGEToGEGE a b)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (x : B), (F.mapIdIso x).hom = F.mapId x
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Raw.ofList : {α : Type u} →
  {β : α → Type v} →
    List ((a : α) × β a) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.ofList._auto_1) → Std.DTreeMap.Raw α β cmp
-- Init.Data.Nat.Basic
/-- Applies a function to a starting value the specified number of times.

In other words, `f` is iterated `n` times on `a`.

This is a tail-recursive version of `Nat.repeat` that's used at runtime.

Examples:
* `Nat.repeatTR f 3 a = f <| f <| f <| a`
* `Nat.repeatTR (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
Nat.repeatTR : {α : Type u} → (α → α) → ℕ → α → α
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_X_inr : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (s : S₂),
  (MvPolynomial.sumRingEquiv R S₁ S₂) (MvPolynomial.X (Sum.inr s)) = MvPolynomial.C (MvPolynomial.X s)
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- If `f` is a fundamental sequence for a limit ordinal `o` and `g` is normal, then `g ∘ f` is a
fundamental sequence for `g o`.  -/
Ordinal.IsFundamentalSeq.comp_isNormal : ∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : Ordinal.{u_1} → Ordinal.{u_1}} (hg : Order.IsNormal g),
  Ordinal.IsFundamentalSeq f → Order.IsSuccLimit o → Ordinal.IsFundamentalSeq fun i => ⟨g ↑(f i), ⋯⟩
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ext_iff : ∀ {X Y : MagmaCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.eval_zero : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁), F.eval 0 = p₀
-- Mathlib.Order.UpperLower.Prod
LowerSet.coe_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : LowerSet α) (t : LowerSet β),
  ↑(s ×ˢ t) = ↑s ×ˢ ↑t
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.next.inj : ∀ {guard : Lean.Expr} {pending : List Lean.Meta.Grind.TheoremGuard} {guard_1 : Lean.Expr}
  {pending_1 : List Lean.Meta.Grind.TheoremGuard},
  Lean.Meta.Grind.ActivateNextGuardResult.next guard pending =
      Lean.Meta.Grind.ActivateNextGuardResult.next guard_1 pending_1 →
    guard = guard_1 ∧ pending = pending_1
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- Convergence in Lp implies convergence in measure.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_Lp : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [hp : Fact (1 ≤ p)] {f : ι → ↥(MeasureTheory.Lp E p μ)} {g : ↥(MeasureTheory.Lp E p μ)}
  {l : Filter ι}, Filter.Tendsto f l (nhds g) → MeasureTheory.TendstoInMeasure μ (fun n => ↑↑(f n)) l ↑↑g
-- Batteries.Data.List.Lemmas
List.countPBefore_eq_countP_take : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ}, List.countPBefore p xs i = List.countP p (List.take i xs)
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected space, if a symmetric transitive relation `P x y` is true for `y` close
enough to `x`, then it holds for all `x, y`. This is a version of the fact that, if an equivalence
relation has open classes, then it has a single equivalence class.  -/
PreconnectedSpace.induction₂ : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] (P : α → α → Prop) [Std.Symm P],
  (∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y) → IsTrans α P → ∀ (x y : α), P x y
-- Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
_private.Mathlib.LinearAlgebra.Multilinear.FiniteDimensional.0.MultilinearMap.free_and_finite : ∀ {ι : Type u_1} {R : Type u_2} {M₂ : Type u_3} {M₁ : ι → Type u_4} [Finite ι] [inst : CommRing R]
  [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂] [Module.Finite R M₂] [Module.Free R M₂]
  [inst_5 : (i : ι) → AddCommGroup (M₁ i)] [inst_6 : (i : ι) → Module R (M₁ i)] [∀ (i : ι), Module.Finite R (M₁ i)]
  [∀ (i : ι), Module.Free R (M₁ i)], Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.mem_of_hasInductedTStructure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [inst_6 : P.IsTriangulated] (t : CategoryTheory.Triangulated.TStructure C)
  [P.IsClosedUnderIsomorphisms] [P.HasInducedTStructure t],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ), n₀ + 1 = n₁ → t.IsLE T.obj₁ n₀ → P T.obj₂ → t.IsGE T.obj₃ n₁ → P T.obj₁ ∧ P T.obj₃
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β), κ.sectL b = κ.comap (fun a => (a, b)) ⋯
-- Mathlib.MeasureTheory.Integral.IntegrableOn
Continuous.integrableAt_nhds : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace α]
  [SecondCountableTopologyEither α E] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → E},
  Continuous f → ∀ (a : α), MeasureTheory.IntegrableAtFilter f (nhds a) μ
-- Init.Data.Array.Lemmas
/-- Variant of `all_filterMap` with a side condition for the `stop` argument.  -/
Array.all_filterMap' : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {xs : Array α} {f : α → Option β} {p : β → Bool},
  stop = (Array.filterMap f xs).size →
    (Array.filterMap f xs).all p 0 stop =
      xs.all fun a =>
        match f a with
        | some b => p b
        | none => true
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rankTR_eq : @Batteries.BinomialHeap.Imp.HeapNode.rankTR = @Batteries.BinomialHeap.Imp.HeapNode.rank
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.comp_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {X_1 Y Z : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (f : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X X_1 Y)
  (g : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom X Y Z) (X_2 : X),
  (CategoryTheory.CategoryStruct.comp f g).snd.app X_2 =
    CategoryTheory.CategoryStruct.comp (f.snd.app X_2) (g.snd.app X_2)
-- Mathlib.Data.Nat.BinaryRec
Nat.binaryRecFromOne.eq_1 : ∀ {motive : ℕ → Sort u} (zero : motive 0) (one : motive 1)
  (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (Nat.bit b n)) (n : ℕ),
  Nat.binaryRecFromOne zero one bit n =
    Nat.binaryRec' zero
      (fun b n h ih =>
        if h' : n = 0 then
          have this := ⋯;
          ⋯ ▸ one
        else bit b n h' ih)
      n
-- Std.Time.Format.Modifier
Std.Time.ZoneId.full.sizeOf_spec : sizeOf Std.Time.ZoneId.full = 1
-- Init.Data.List.Sublist
List.IsSuffix.map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) ⦃l₁ l₂ : List α⦄, l₁ <:+ l₂ → List.map f l₁ <:+ List.map f l₂
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff : ∀ {S X₁ X₂ : Type u} (f : S ⟶ X₁) (g : S ⟶ X₂) (x₂ y₂ : X₂),
  CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B},
  Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π) → CategoryTheory.EffectiveEpiFamily X π
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.evaluation_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ)
  {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y), (PresheafOfModules.evaluation R X).map f = f.app X
-- Std.Data.Internal.List.Associative
Std.Internal.List.minEntry?_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minEntry? (Std.Internal.List.replaceEntry k v l) =
      Option.map (fun e => if (e.fst == k) = true then ⟨k, v⟩ else e) (Std.Internal.List.minEntry? l)
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroInt16SintOfNatNat : Lean.Grind.ToInt.Zero Int16 (Lean.Grind.IntInterval.sint 16)
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.to_map_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {x : R}, (algebraMap R K) x = 0 ↔ x = 0
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.one_lt_prod : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelMonoid M] {f : ι → M}, 1 < f → 1 < ∏ i, f i
-- Mathlib.Algebra.Group.Units.Opposite
isAddUnit_op : ∀ {M : Type u_2} [inst : AddMonoid M] {m : M}, IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_inf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] (s t : ClosedSubmodule R M), ↑(s ⊓ t) = ↑s ⊓ ↑t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.add_def : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point), P + Q = P.add Q
-- Init.Data.UInt.Lemmas
UInt32.mod_self : ∀ {a : UInt32}, a % a = 0
-- Init.Data.SInt.Basic
/-- Constructs an `ISize` from an `Int`, clamping if the value is too small or too large.  -/
ISize.ofIntTruncate : ℤ → ISize
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSMul : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → {K : Type u_5} → [SMul K β] → SMul K (MeasureTheory.SimpleFunc α β)
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A ring is semisimple if it is semisimple as a module over itself.  -/
IsSemisimpleRing : (R : Type u_2) → [Ring R] → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.ofList l) k fallback = fallback
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.unsat_of_convertLRAT_unsat : ∀ (cnf : Std.Sat.CNF ℕ),
  Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin (cnf.numLiterals + 1))
      (Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT cnf) →
    cnf.Unsat
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffOn.curry_right`.

---

Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffOn.along_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {s : Set (M × M')},
  ContMDiffOn (I.prod I') J n (Function.uncurry f) s → ContMDiffOn I' J n (fun y => f x y) {y | (x, y) ∈ s}
-- Mathlib.Data.List.OfFn
List.ofFn_fin_append : ∀ {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α), List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLEReflOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Refl fun x1 x2 => x1 ≤ x2], Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.SetNotation
/-- Indexed intersection of a family of sets  -/
Set.iInter : {α : Type u} → {ι : Sort v} → (ι → Set α) → Set α
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.pow_count : ∀ {M : Type u_3} [inst : CommMonoid M] {s : Multiset M} [inst_1 : DecidableEq M] (a : M),
  a ^ Multiset.count a s = (Multiset.filter (Eq a) s).prod
-- Mathlib.Order.BooleanAlgebra.Set
Set.instHImp : {α : Type u_1} → HImp (Set α)
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.le_spanNorm_spanNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (T : Type u_4) [inst_9 : CommRing T] [inst_10 : IsDomain T]
  [inst_11 : IsIntegrallyClosed T] [inst_12 : Algebra R T] [inst_13 : Algebra T S] [inst_14 : Module.Finite R T]
  [inst_15 : Module.Finite T S] [inst_16 : Module.IsTorsionFree R T] [inst_17 : Module.IsTorsionFree T S]
  [IsScalarTower R T S] (I : Ideal S), Ideal.spanNorm R I ≤ Ideal.spanNorm R (Ideal.spanNorm T I)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.lt : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfOrdArgs α) →
    let this := self.ord;
    LT α