mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- Variant of `ιFunctorObj_extension` where the diagram involving `functorObj f πX`
is replaced by an isomorphic diagram.  -/
CategoryTheory.SmallObject.ιFunctorObj_extension' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  {πX : X ⟶ S}
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  {X' S' Z' : C} (πX' : X' ⟶ S') (ι' : X' ⟶ Z') (πZ' : Z' ⟶ S'),
  CategoryTheory.CategoryStruct.comp ι' πZ' = πX' →
    ∀ (eX : X' ≅ X) (eS : S' ≅ S) (eZ : Z' ≅ CategoryTheory.SmallObject.functorObj f πX),
      CategoryTheory.CategoryStruct.comp ι' eZ.hom =
          CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.SmallObject.ιFunctorObj f πX) →
        CategoryTheory.CategoryStruct.comp πZ' eS.hom =
            CategoryTheory.CategoryStruct.comp eZ.hom (CategoryTheory.SmallObject.πFunctorObj f πX) →
          ∀ {i : I} (t : A i ⟶ X') (b : B i ⟶ S'),
            CategoryTheory.CategoryStruct.comp t πX' = CategoryTheory.CategoryStruct.comp (f i) b →
              ∃ l,
                CategoryTheory.CategoryStruct.comp (f i) l = CategoryTheory.CategoryStruct.comp t ι' ∧
                  CategoryTheory.CategoryStruct.comp l πZ' = b
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.tooltip? : Lean.Elab.InlayHintInfo → Option String
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t → t.max?.isSome = true
-- Mathlib.Order.Filter.Map
Filter.eventually_pure : ∀ {α : Type u_1} {a : α} {p : α → Prop}, (∀ᶠ (x : α) in pure a, p x) ↔ p a
-- Mathlib.Order.PiLex
Pi.apply_le_of_toLex : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x y : (i : ι) → β i} {i : ι}
  [inst_1 : (i : ι) → LinearOrder (β i)], toLex x ≤ toLex y → (∀ j < i, x j = y j) → x i ≤ y i
-- Init.Grind.AC
Lean.Grind.AC.eq_erase_dup_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_erase_dup_cert lhs rhs lhs' rhs' = (lhs.eraseDup.beq' lhs').and' (rhs.eraseDup.beq' rhs')
-- Mathlib.Data.Int.Bitwise
Function.swap.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α),
  Function.swap f y x = f x y
-- Std.Do.SPred.SPred
/-- Logical equivalence of `SPred`.

Logically equivalent predicates are equal. Use `SPred.bientails.to_eq` to convert bi-entailment to
equality.
 -/
Std.Do.SPred.bientails : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Prop
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instCoeFunForall.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N], AddEquiv.instCoeFunForall = { coe := fun f => ⇑f }
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {s t : Set β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → s ≤ᵐ[μb] t → f ⁻¹' s ≤ᵐ[μa] f ⁻¹' t
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.cosh_bijOn : Set.BijOn Real.cosh (Set.Ici 0) (Set.Ici 1)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} {X Y : CategoryTheory.GradedObject β C}
  (f g : X ⟶ Y), (∀ (x : β), f x = g x) → f = g
-- Lean.CoreM
Lean.Core.getMessageLog : Lean.CoreM Lean.MessageLog
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.symm_dual_id : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α],
  BoundedOrderHom.dual.symm (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  [inst_2 : Inhabited (γ k)], (Std.ExtDTreeMap.filterMap f t).get! k = ((t.get? k).bind (f k)).get!
-- Mathlib.Order.CompleteLattice.Basic
Monotone.le_map_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β]
  {f : α → β}, Monotone f → ⨆ i, f (s i) ≤ f (iSup s)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ), (x ^ n).valuation = n * x.valuation
-- Init.Prelude
/-- Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt8` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : UInt8) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : UInt8) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : UInt8) < 7) by decide`
 -/
UInt8.decLt : (a b : UInt8) → Decidable (a < b)
-- Mathlib.Analysis.Polynomial.Norm
Polynomial.exists_eq_supNorm : ∀ {A : Type u_1} [inst : SeminormedRing A] (p : Polynomial A), ∃ i, p.supNorm = ‖p.coeff i‖
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportedByParams.mk.sizeOf_spec : ∀ (module : Lean.Lsp.LeanModule), sizeOf { module := module } = 1 + sizeOf module
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.Hom.mk.inj : ∀ {k : Type u} {G : Type v} {inst : TopologicalSpace k} {inst_1 : Ring k} {inst_2 : Monoid G} {A : TopRep k G}
  {B : TopRep k G} {hom' hom'_1 : ContIntertwiningMap A.ρ B.ρ}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.isSatisfiable_onTheory_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'},
  φ.Injective → ((φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_hom_nonempty : ∀ {M : Type u_4} {N : Type u_5} [inst : AddMonoid M] [inst_1 : AddMonoid N] {l : List M} {F : Type u_8}
  [inst_2 : FunLike F M N] [AddHomClass F M N] (f : F), l ≠ [] → (List.map (⇑f) l).sum = f l.sum
-- Mathlib.NumberTheory.SmoothNumbers
/-- The non-zero non-`s`-factored numbers are `≥ N` when `s` contains all primes less than `N`.  -/
Nat.factoredNumbers_compl : ∀ {N : ℕ} {s : Finset ℕ}, N.primesBelow ⊆ s → (Nat.factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.mem_hasEvalIdeal_iff : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [inst_2 : IsTopologicalRing S]
  [inst_3 : IsLinearTopology S S] {a : σ → S}, a ∈ MvPowerSeries.hasEvalIdeal ↔ MvPowerSeries.HasEval a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_rcc : ∀ {a b : ℕ}, (a...=b).toArray.size = b + 1 - a
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.α_pow : ∀ {q : ℕ} (i : ℕ), LucasLehmer.X.α ^ (2 * i + 1) = 3 ^ i * LucasLehmer.X.α
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 < ⌊a⌋₊ ↔ 1 ≤ a
-- Mathlib.Order.RelSeries
RelSeries.instNonempty : ∀ {α : Type u_1} (r : SetRel α α) [Nonempty α], Nonempty (RelSeries r)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.ColimitOfShape J X → CategoryTheory.Limits.ColimitPresentation J X
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.listL.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (parent : RBTree.RBNode.Path α) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (v : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l v parent)),
  (match RBTree.RBNode.Path.right c l v parent with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent v r => h_2 c parent v r
    | RBTree.RBNode.Path.right c l v parent => h_3 c l v parent) =
    h_3 c l v parent
-- Init.Grind.ToInt
Lean.Grind.ToInt.LE.mk : ∀ {α : Type u} [inst : LE α] {I : outParam Lean.Grind.IntInterval} [inst_1 : Lean.Grind.ToInt α I],
  (∀ (x y : α), x ≤ y ↔ ↑x ≤ ↑y) → Lean.Grind.ToInt.LE α I
-- Init.Data.UInt.Bitwise
UInt8.toUSize_or : ∀ (a b : UInt8), (a ||| b).toUSize = a.toUSize ||| b.toUSize
-- Init.Data.List.Lemmas
List.append_ne_nil_of_right_ne_nil : ∀ {α : Type u_1} {t : List α} (s : List α), t ≠ [] → s ++ t ≠ []
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
  (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})],
  P = Ideal.span {hζ.toInteger - 1}
-- Mathlib.Topology.Order.LeftRightNhds
/-- The set of points in a set which are isolated on the left in this set is countable when the
space is second-countable.  -/
countable_setOfPred_isolated_left_within : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α}, {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Iio x) = ⊥}.Countable
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  (h' : a ∈ t), t.getKey? a = some (t.getKey a h')
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.sqrt : Nat.Primrec' fun v => v.head.sqrt
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearMap.fixedSubmodule_eq_top_iff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {f : V →ₗ[R] V},
  f.fixedSubmodule = ⊤ ↔ f = LinearMap.id
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.isSameSolverTerms.unsafe_1 : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Bool
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).v₂₃.τ₁ = CategoryTheory.Limits.cokernel.π f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext.mk : Bool → Lean.Lsp.ReferenceContext
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_snd_apply : ∀ (X Y : TopCat) (x : ↑X × ↑Y),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)
      ((CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).inv) x) =
    x.2
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (m.insertManyIfNewUnit l).size = m.size + l.length
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.prod_bot_right : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : AffineSubspace k P), s.prod ⊥ = ⊥
-- Lean.Data.NameTrie
Lean.NameTrie.foldM : {m : Type u_1 → Type u_2} → {β : Type u_3} → {σ : Type u_1} → [Monad m] → Lean.NameTrie β → σ → (β → σ → m σ) → m σ
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.ker_liftQ_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ f.ker), f.ker ≤ p → (p.liftQ f h).ker = ⊥
-- Mathlib.Data.Sigma.Basic
/-- A version of `Iff.mp Sigma.ext_iff` for functions from a nonempty type to a sigma type.  -/
Function.eq_of_sigmaMk_comp : ∀ {α : Type u_1} {β : α → Type u_4} {γ : Type u_7} [Nonempty γ] {a b : α} {f : γ → β a} {g : γ → β b},
  Sigma.mk a ∘ f = Sigma.mk b ∘ g → a = b ∧ f ≍ g
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.equivOfIsometry_refl : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  {Q₁ : QuadraticForm R M₁}, CliffordAlgebra.equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl
-- Mathlib.CategoryTheory.Limits.FunctorToTypes
CategoryTheory.FunctorToTypes.jointly_surjective : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K (Type w))) (k : K) {t : CategoryTheory.Limits.Cocone F}
  (h : CategoryTheory.Limits.IsColimit t) (x : t.pt.obj k) [∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.obj k)],
  ∃ j y, x = (CategoryTheory.ConcreteCategory.hom ((t.ι.app j).app k)) y
-- Mathlib.Analysis.Analytic.Composition
AnalyticAt.comp_analyticWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E} {s : Set E},
  AnalyticAt 𝕜 g (f x) → AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 (g ∘ f) s x
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.forIn'.loop.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.inv₀_iff : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] (x : R), IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.ae_withDensity_iff_ae_restrict' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal},
  AEMeasurable f μ → ((∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x | f x ≠ 0}, p x)
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E) (h : x ≠ 0) (a : ↥(𝕜 ∙ x)),
  (ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h).symm a =
    (LinearEquiv.ofInjective (LinearMap.toSpanSingleton 𝕜 E x) ⋯).symm
      ((LinearEquiv.ofEq (𝕜 ∙ x) (LinearMap.toSpanSingleton 𝕜 E x).range ⋯) a)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural_right : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X' X)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
      (CategoryTheory.Functor.OplaxMonoidal.δ F X' Y)
-- Mathlib.Order.Lex
instNonemptyLex : ∀ (α : Type u_2) [Nonempty α], Nonempty (Lex α)
-- Lean.Syntax
Lean.Syntax.MonadTraverser.goDown : {m : Type → Type} → [t : Lean.Syntax.MonadTraverser m] → ℕ → m Unit
-- Mathlib.Order.Interval.Finset.Nat
Nat.pow_imp_self_of_one_lt : ∀ {M : Type u_1} [inst : Monoid M] (k : ℕ),
  1 < k →
    ∀ (P : M → Prop),
      (∀ (x y : M), P x → P (x * y) ∨ P (y * x)) → (∀ (x : M), P (x ^ k) → P x) → ∀ (n : ℕ) (x : M), P (x ^ n) → P x
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.linearEquiv_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] (G : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι] [inst_6 : IsDirectedOrder ι]
  [inst_7 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] {i : ι} {g : G i},
  (Module.DirectLimit.linearEquiv G f) ((Module.DirectLimit.of R ι G f i) g) = ⟦⟨i, g⟩⟧
-- Lean.Meta.Basic
Lean.Meta.State.mk.sizeOf_spec : ∀ (mctx : Lean.MetavarContext) (cache : Lean.Meta.Cache) (zetaDeltaFVarIds : Lean.FVarIdSet)
  (postponed : Lean.PersistentArray Lean.Meta.PostponedEntry) (diag : Lean.Meta.Diagnostics),
  sizeOf { mctx := mctx, cache := cache, zetaDeltaFVarIds := zetaDeltaFVarIds, postponed := postponed, diag := diag } =
    1 + sizeOf mctx + sizeOf cache + sizeOf zetaDeltaFVarIds + sizeOf postponed + sizeOf diag
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.min_le_mk_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a b : M),
  min (ArchimedeanClass.mk a) (ArchimedeanClass.mk b) ≤ ArchimedeanClass.mk (a + b)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_unit : AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.unit = AlgebraicGeometry.identityToΓSpec
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.J.eq_1 : UpperHalfPlane.J = Matrix.GeneralLinearGroup.mkOfDetNeZero !![-1, 0; 0, 1] UpperHalfPlane.J._proof_1
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsInf` of a filter `f` is the least cluster point of `f`.  -/
isLeast_clusterPt_limsInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} [f.NeBot],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f) isLeast_clusterPt_limsInf._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) isLeast_clusterPt_limsInf._auto_3 →
      IsLeast {x | ClusterPt x f} f.limsInf
-- Mathlib.Order.Basic
/-- **Alias** of `le_trans`. -/
ge_trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_functor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) {X Y : C} (f : X ⟶ Y), e.rightOp.functor.map f = (e.functor.map f.op).op
-- Mathlib.Computability.Reduce
OneOneEquiv.congr_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, OneOneEquiv q r → (OneOneEquiv p q ↔ OneOneEquiv p r)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.subset_one_iff : ∀ {α : Type u_2} [inst : One α] {s : Set α}, s.Nonempty → (s ⊆ 1 ↔ s = 1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkip?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos res : s.Pos},
  pos.revSkip? P = some res ↔ ∃ (h : pos ≠ s.startPos), res = pos.prev h ∧ P ((pos.prev h).get ⋯)
-- Lean.LocalContext
Lean.instInhabitedLocalDecl : Inhabited Lean.LocalDecl
-- Std.Http.Data.Body.Full
/-- Builds a response with a JSON body.
Sets `Content-Type: application/json`.
 -/
Std.Http.Response.Builder.json : Std.Http.Response.Builder → String → Std.Async.Async (Std.Http.Response Std.Http.Body.Full)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C)
  (G : CategoryTheory.StrictlyUnitaryLaxFunctor C D) (a : B),
  (F.comp G).mapId a = CategoryTheory.CategoryStruct.comp (G.mapId (F.obj a)) (G.map₂ (F.mapId a))
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.binEntropy_one : Real.binEntropy 1 = 0
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.instSemilatticeInf : {ι : Type u_1} → {I : BoxIntegral.Box ι} → SemilatticeInf (BoxIntegral.Prepartition I)
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.applyComposition_apply_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E] {H : Type u_6}
  [inst_6 : CommRing H] [inst_7 : Algebra 𝕜 H] [inst_8 : TopologicalSpace H] [inst_9 : IsTopologicalRing H]
  [inst_10 : ContinuousConstSMul 𝕜 H] (p : FormalMultilinearSeries 𝕜 E H) {n : ℕ} (c : Composition n) (v : Fin n → E),
  ∏ i, p.applyComposition c v i = ∏ i, (p (c.blocksFun i)) (v ∘ ⇑(c.embedding i))
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_succ : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M] (k : ℕ), LieSubmodule.ucs (k + 1) N = (LieSubmodule.ucs k N).normalizer
-- Init.Data.Dyadic.Basic
Dyadic.precision_neg : ∀ {x : Dyadic}, (-x).precision = x.precision
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α) (hlk : k ∈ t),
  t.getEntry k hlk =
    match t, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk =>
      match h : compare k k' with
      | Ordering.lt => l.getEntry k ⋯
      | Ordering.gt => r.getEntry k ⋯
      | Ordering.eq => ⟨k', v'⟩
-- Mathlib.Order.Filter.Pointwise
Filter.mem_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter β} {s : Set β} {a : α},
  s ∈ a • f ↔ (fun x => a • x) ⁻¹' s ∈ f
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace β} (b : β), MeasurableSpace.comap (fun _a => b) m = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.condition : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Cofork f g),
  CategoryTheory.CategoryStruct.comp f t.π = CategoryTheory.CategoryStruct.comp g t.π
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.ratio_le_opNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) (m : ι → E), ‖f m‖ / ∏ i, ‖m i‖ ≤ ‖f‖
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_right_anti₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀],
  0 ≤ a → a ≤ 1 → Antitone fun n => a ^ n
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.eq_of_infinite_eval_eq : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] (p q : Polynomial R),
  {x | Polynomial.eval x p = Polynomial.eval x q}.Infinite → p = q