mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- A functor `G : C ⥤ D` sends cones over `F` to cones over `F ⋙ G` functorially.  -/
CategoryTheory.Limits.Cone.functoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (G : CategoryTheory.Functor C D) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (F.comp G))
-- Lean.Syntax
Lean.Syntax.isAntiquotSuffixSplice : Lean.Syntax → Bool
-- Mathlib.Topology.ContinuousMap.T0Sierpinski
TopologicalSpace.productOfMemOpens_injective : ∀ (X : Type u_1) [inst : TopologicalSpace X] [T0Space X], Function.Injective ⇑(TopologicalSpace.productOfMemOpens X)
-- Mathlib.Data.List.Pairwise
List.Pairwise.forall_of_forall : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Symm R],
  (∀ x ∈ l, R x x) → List.Pairwise R l → ∀ ⦃x : α⦄, x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.match.inj : ∀ {ref gen discrs optMotive : Lean.Syntax} {alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)}
  {ref_1 gen_1 discrs_1 optMotive_1 : Lean.Syntax} {alts_1 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)},
  Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts =
      Lean.Elab.Term.Do.Code.match ref_1 gen_1 discrs_1 optMotive_1 alts_1 →
    ref = ref_1 ∧ gen = gen_1 ∧ discrs = discrs_1 ∧ optMotive = optMotive_1 ∧ alts = alts_1
-- Mathlib.Probability.Decision.BayesEstimator
/-- Given an argmin estimator `f`, we can define a deterministic kernel.  -/
ProbabilityTheory.IsArgminEstimator.kernel : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} →
            {ℓ : Θ → 𝓨 → ENNReal} →
              {P : ProbabilityTheory.Kernel Θ 𝓧} →
                {π : MeasureTheory.Measure Θ} →
                  [inst : StandardBorelSpace Θ] →
                    [inst_1 : Nonempty Θ] →
                      {f : 𝓧 → 𝓨} →
                        [inst_2 : ProbabilityTheory.IsFiniteKernel P] →
                          [inst_3 : MeasureTheory.IsFiniteMeasure π] →
                            ProbabilityTheory.IsArgminEstimator ℓ P π f → ProbabilityTheory.Kernel 𝓧 𝓨
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_zero_of_not_uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, ¬UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = 0
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `monomial s a` is the monomial with coefficient `a` and exponents given by `s`  -/
MvPolynomial.monomial : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → (σ →₀ ℕ) → R →ₗ[R] MvPolynomial σ R
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_f_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0)
  (p q : ℤ) (hpq : p + -1 = q) {Z : C} (h : L.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.snd φ).v p q hpq) h) =
    CategoryTheory.CategoryStruct.comp (β.v p q hpq) h
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_coeff : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} (i : ℕ),
  f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
/-- `List.antidiagonalTuple k n` is a list of all `k`-tuples which sum to `n`.

This list contains no duplicates (`List.Nat.nodup_antidiagonalTuple`), and is sorted
lexicographically (`List.Nat.antidiagonalTuple_pairwise_pi_lex`), starting with `![0, ..., n]`
and ending with `![n, ..., 0]`.

```
#eval antidiagonalTuple 3 2
-- [![0, 0, 2], ![0, 1, 1], ![0, 2, 0], ![1, 0, 1], ![1, 1, 0], ![2, 0, 0]]
```
 -/
List.Nat.antidiagonalTuple : (k : ℕ) → ℕ → List (Fin k → ℕ)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.mk.injEq : ∀ (toSheafedSpace : AlgebraicGeometry.SheafedSpace CommRingCat)
  (isLocalRing : ∀ (x : ↑↑toSheafedSpace.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace.presheaf.stalk x))
  (toSheafedSpace_1 : AlgebraicGeometry.SheafedSpace CommRingCat)
  (isLocalRing_1 : ∀ (x : ↑↑toSheafedSpace_1.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace_1.presheaf.stalk x)),
  ({ toSheafedSpace := toSheafedSpace, isLocalRing := isLocalRing } =
      { toSheafedSpace := toSheafedSpace_1, isLocalRing := isLocalRing_1 }) =
    (toSheafedSpace = toSheafedSpace_1)
-- Mathlib.RingTheory.Polynomial.Nilpotent
/-- Let `P` be a polynomial over `R`. If its constant term is a unit and its other coefficients are
nilpotent, then `P` is a unit.

See also `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent`.  -/
Polynomial.isUnit_of_coeff_isUnit_isNilpotent : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
  IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → IsUnit P
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback fallback' : α},
        Std.Internal.List.getKeyD (Std.Internal.List.minKeyD l fallback) l fallback' =
          Std.Internal.List.minKeyD l fallback
-- Init.Internal.Order.Basic
Lean.Order.admissible_pprod_fst : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] (P : α → Prop),
  Lean.Order.admissible P → Lean.Order.admissible fun x => P x.fst
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.ext : ∀ {R : Type u_1} [inst : SeminormedCommRing R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S]
  {p q : AlgebraNorm R S}, (∀ (x : S), p x = q x) → p = q
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.eq_1 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match none with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_1 ()
-- Lean.Syntax
Lean.Syntax.mkAntiquotSpliceNode : Lean.SyntaxNodeKind → Array Lean.Syntax → String → optParam ℕ 0 → Lean.Syntax
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on
overflow.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.ofNat : ℕ → ISize
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.forget_createsLimitsOfShape.eq_1 : ∀ (J : Type v) [inst : CategoryTheory.Category.{w, v} J],
  AddCommGrpCat.forget_createsLimitsOfShape J = { CreatesLimit := fun {K} => inferInstance }
-- Std.Time.Zoned.Database.Basic
/-- Converts a Boolean value to a corresponding `UTLocal` type.
 -/
Std.Time.TimeZone.convertUt : Bool → Std.Time.TimeZone.UTLocal
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.re_natCast : ∀ {d : ℤ} (n : ℕ), (↑n).re = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_inv_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp h.isoPullback.inv snd = CategoryTheory.Limits.pullback.snd f g
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.saturateCore.go : Aesop.LocalRuleSet → Lean.MVarId → Aesop.SaturateM Lean.MVarId
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.piCongrRight_refl : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)],
  (LinearEquiv.piCongrRight fun j => LinearEquiv.refl R (φ j)) = LinearEquiv.refl R ((i : ι) → φ i)
-- Mathlib.Data.Nat.Factorization.Root
/-- Ceiling root of a natural number. This divides the valuation of every prime number rounding up.

Eg if `n = 3`, `a = 2^4 * 3^2 * 5`, then `ceilRoot n a = 2^2 * 3 * 5`.

In order theory terms, this is the lower or left adjoint of the map `a ↦ a ^ n : ℕ → ℕ` where `ℕ`
is ordered by divisibility.

To ensure that the adjunction (`Nat.dvd_pow_iff_ceilRoot_dvd`) holds in as many cases as possible,
we special-case the following values:
* `ceilRoot 0 a = 0` (this one is not strictly necessary)
* `ceilRoot n 0 = 0`
 -/
Nat.ceilRoot : ℕ → ℕ → ℕ
-- Mathlib.Data.Finset.Slice
Finset.biUnion_slice : ∀ {α : Type u_1} (𝒜 : Finset (Finset α)) [inst : Fintype α] [inst_1 : DecidableEq α],
  (Finset.Iic (Fintype.card α)).biUnion 𝒜.slice = 𝒜
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_addEquivProd : ∀ {R : Type u_3} [inst : Add R] (c₁ c₂ c₃ : R),
  ⇑(QuaternionAlgebra.addEquivProd c₁ c₂ c₃) = ⇑(QuaternionAlgebra.equivProd c₁ c₂ c₃)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `CommMonoid` homs `g : M →* P, l : P →* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
Submonoid.LocalizationMap.map_comp_map : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : CommMonoid A]
  {U : Submonoid A} {R : Type u_6} [inst_5 : CommMonoid R] (j : U.LocalizationMap R) {l : P →* A}
  (hl : ∀ (w : ↥T), l ↑w ∈ U), (k.map hl j).comp (f.map hy k) = f.map ⋯ j
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- We'd like to state this as `L.headI + L.tail.sum = L.sum`, but because `L.headI`
relies on an inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of `L[0]?.getD 0`.  -/
List.getElem?_zero_add_tail_sum : ∀ {M : Type u_4} [inst : AddMonoid M] (l : List M), l[0]?.getD 0 + l.tail.sum = l.sum
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.comap_mulValuation_eq_padicValuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Valuation.comap (Rat.castHom ℚ_[p]) Padic.mulValuation = Rat.padicValuation p
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.prodLIE_symm_apply : ∀ (𝕜 : Type u) (E : Type wE) (F : Type wF) (G : Type wG) {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : E [⋀^ι]→L[𝕜] (F × G)),
  (ContinuousAlternatingMap.prodLIE 𝕜 E F G).symm f =
    ((ContinuousLinearMap.fst 𝕜 F G).compContinuousAlternatingMap f,
      (ContinuousLinearMap.snd 𝕜 F G).compContinuousAlternatingMap f)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.ofHom_comp : ∀ {R : Type u} [inst : Ring R] {M N O : Type v} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup O] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R O] (f : M →ₗ[R] N)
  (g : N →ₗ[R] O), ModuleCat.ofHom (g ∘ₗ f) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom f) (ModuleCat.ofHom g)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.epi_of_epi_of_epi_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 3} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Epi
          (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_13) →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_4) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 3 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_7) →
            CategoryTheory.Epi
              (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_11)
-- Mathlib.Data.List.OfFn
List.equivSigmaTuple_apply_snd : ∀ {α : Type u} (l : List α) (a : Fin l.length), (List.equivSigmaTuple l).snd a = l.get a
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.congr_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ}, k = l → p k = 0 → p l = 0
-- Mathlib.RingTheory.Valuation.Integers
/-- The ideal of elements of the valuation subring whose valuation is less than or equal to a
certain value.  -/
Valuation.leIdeal : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → Γ₀ → Ideal ↥v.integer
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_mul : ∀ {α : Type u_1} [inst : Semiring α] {f : α → α → α} {a b : α} {a' b' c : ℕ},
  f = HMul.hMul →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.mul b' = c → Mathlib.Meta.NormNum.IsNat (a * b) c
-- Mathlib.Computability.Reduce
ULower.down_computable : ∀ {α : Type u_1} [inst : Primcodable α], (ULower.equiv α).Computable
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.span_singleton_dvd_span_singleton_iff_dvd`. -/
span_singleton_dvd_span_singleton_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R},
  Ideal.span {a} ∣ Ideal.span {b} ↔ a ∣ b
-- Init.Data.Iterators.Combinators.FlatMap
/-- Let `it₁` and `it₂` be iterators and `f` a monadic function mapping `it₁`'s outputs to iterators
of the same type as `it₂`. Then `it₁.flatMapAfterM f it₂` first goes over `it₂` and then over
`it₁.flatMap f it₂`, emitting all their values.

The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
that is currently iterating over one of the inner iterators.

**Marble diagram (without monadic effects):**

```text
it₁                            --b      c    --d -⊥
it₂                      a1-a2⊥
f b                               b1-b2⊥
f c                                      c1-c2⊥
f d                                             ⊥
it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
iterator.

For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
Std.Iter.flatMapAfterM : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : MonadAttach m] →
        [Std.Iterator α Id β] →
          [Std.Iterator α₂ m γ] → (f : β → m (Std.IterM m γ)) → Std.Iter β → Option (Std.IterM m γ) → Std.IterM m γ
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.natDegree_zero_le : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.natDegree 0 ≤ 0
-- Mathlib.Computability.Language
/-- Zero language has no elements.  -/
Language.instZero : {α : Type u_1} → Zero (Language α)
-- Mathlib.Algebra.Group.Basic
div_div_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a / (a / b) = b
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.symm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → AntivaryOn g f s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RoiSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Roi α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Roi α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.Finite.evaluation_preservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesFiniteColimits (PresheafOfModules.evaluation R X)
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Get the smallest element in the tree that is `> x`.

```
findGt 2 {1, 2, 4} = some 4
findGt 3 {1, 2, 4} = some 4
findGt 4 {1, 2, 4} = none
```  -/
Ordnode.findGt : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Option α
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.instSyzygies : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.EnoughProjectives C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y)
  [inst_3 : CategoryTheory.Limits.HasKernel f], CategoryTheory.Projective (CategoryTheory.Projective.syzygies f)
-- Init.Data.Order.Lemmas
Std.Asymm.total_not : ∀ {α : Sort u_1} {r : α → α → Prop} [i : Std.Asymm r], Std.Total fun x1 x2 => ¬r x1 x2
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.op_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) (a : Aᵐᵒᵖ),
  (AlgEquiv.op f) a = MulOpposite.op (f (MulOpposite.unop a))
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.ext_iff : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {φ₁ φ₂ : (PiTensorProduct R fun i => s i) →ₗ[R] E},
  φ₁ = φ₂ ↔ φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N K : CategoryTheory.Mon C} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : SemilatticeInf β] [inst_3 : ContinuousInf β] (f g : α →ₘ[μ] β), ↑(f ⊓ g) =ᵐ[μ] fun x => ↑f x ⊓ ↑g x
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.rightHom_section : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (σ : S.Section) (g : G), S.rightHom (σ g) = g
-- Init.Data.BitVec.Lemmas
BitVec.toFin_ofNat : ∀ {w : ℕ} (x : ℕ), (BitVec.ofNat w x).toFin = Fin.ofNat (2 ^ w) x
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTOfNatNatOfProjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.Projective X], CategoryTheory.HasProjectiveDimensionLT X 1
-- Mathlib.Topology.Order.Basic
Filter.Eventually.exists_Ioo_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α]
  {a : α} {p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ {x | p x}
-- Mathlib.Control.Functor
Functor.AddConst.lawfulFunctor : ∀ {γ : Type u_1}, LawfulFunctor (Functor.AddConst γ)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
/-- This type is used in lemmas about iterator equivalence (`Iter.Equiv` and `IterM.Equiv`).

`it.QuotStep` is the quotient of `it.Step` where two steps are identified if they agree up to
equivalence of their successor iterator.
 -/
Std.IterM.QuotStep : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} → [Std.Iterator α m β] → [inst : Monad m] → [LawfulMonad m] → Std.IterM m β → Type u_1
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.compEvaluation_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (b : B) (X : A),
  (CategoryTheory.compEvaluation F b).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj b)
-- Init.Data.UInt.Lemmas
UInt16.ofNatTruncate_uInt8ToNat : ∀ (n : UInt8), UInt16.ofNatClamp n.toNat = n.toUInt16
-- Lean.Language.Lean.Types
Lean.Language.Lean.HeaderParsedSnapshot.toSnapshot : Lean.Language.Lean.HeaderParsedSnapshot → Lean.Language.Snapshot
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.twoCocycleOf_coe_coe : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L)
  {s : L →ₗ[R] E.L} (hs : Function.LeftInverse ⇑E.proj ⇑s),
  ↑↑(E.twoCocycleOf hs) = (LieAlgebra.Extension.twoCocycleAux✝ E hs).compr₂ ↑E.toKer.symm.toLinearEquiv
-- Mathlib.Tactic.NormNum.Pow
Mathlib.Meta.NormNum.IsNatPowT.run : ∀ {a b c : ℕ}, Mathlib.Meta.NormNum.IsNatPowT (a.pow 1 = a) a b c → a.pow b = c
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : M),
  (Monoid.Coprod.swap M N) (Monoid.Coprod.inl x) = Monoid.Coprod.inr x
-- Mathlib.Combinatorics.Digraph.Basic
instDecidableRelAdjCoeEmbeddingForallForallBoolDigraphMk' : {V : Type u_1} → (adj : V → V → Bool) → DecidableRel (Digraph.mk' adj).Adj
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.map.eq_1 : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A),
  relations.map = Finsupp.linearCombination A relations.relation
-- Lean.Parser
Lean.PrettyPrinter.Parenthesizer.interpretParserDescr : Lean.ParserDescr → Lean.CoreM Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_of_not_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬b ≤ a → Set.uIcc a b = Set.Icc a b
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.symm_toLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), e.symm.toLinearEquiv = e.toLinearEquiv.symm