mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.contains.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v : β k') → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)),
  (match Std.DTreeMap.Internal.Impl.inner size k' v l r with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v l r => h_2 size k' v l r) =
    h_2 size k' v l r
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.mul_inv_mem_inertia : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {G : Type u_3}
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] {Q : Ideal S} {σ σ' : G},
  IsArithFrobAt R σ Q → IsArithFrobAt R σ' Q → σ * σ'⁻¹ ∈ Ideal.inertia G Q
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.leftUnitor_hom_toNatTrans : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans = F.toFunctor.leftUnitor.hom
-- Init.Prelude
Min.mk : {α : Type u} → (α → α → α) → Min α
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.copyExprMVar : Lean.Meta.SavedState → Lean.MVarId → Lean.MetaM Unit
-- Init.Data.Int.Gcd
Int.gcd_dvd_mul : ∀ (m n : ℤ), ↑(m.gcd n) ∣ m * n
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (root : Lean.PersistentHashMap.Node α β), sizeOf { root := root } = 1 + sizeOf root
-- ImportGraph.Imports.RequiredModules
_private.ImportGraph.Imports.RequiredModules.0.Lean.Environment.transitivelyRequiredModules'.toBitVec : Lean.Environment → {N : ℕ} → Lean.NameSet → BitVec N
-- Mathlib.Data.Sigma.Basic
PSigma.instInhabitedOfDefault_mathlib : {α : Sort u_1} → {β : α → Sort u_2} → [inst : Inhabited α] → [Inhabited (β default)] → Inhabited (PSigma β)
-- Mathlib.Data.Finsupp.Order
Finsupp.sub_add_single_one_cancel : ∀ {ι : Type u_1} {u : ι →₀ ℕ} {i : ι}, u i ≠ 0 → ((u - fun₀ | i => 1) + fun₀ | i => 1) = u
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.Prepartition.compl.congr_simp : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π π_1 : BoxIntegral.Prepartition I),
  π = π_1 → π.compl = π_1.compl
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Adj.darts_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.darts = [{ fst := u, snd := v, adj := h }]
-- Aesop.Search.ExpandSafePrefix
Aesop.SafeExpansionM.State.numRapps : Aesop.SafeExpansionM.State → ℕ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData : ∀ {X : AlgebraicGeometry.Scheme}, CategoryTheory.IsIso ⊥.subschemeι
-- Mathlib.RingTheory.Invariant.Galois
/-- In the AKLB setup, every fixed point of `B` lies in the image of `A`.  -/
Algebra.isInvariant_of_isGalois : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Field K] [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : IsFractionRing A K]
  [IsFractionRing B L] [inst_8 : Algebra A B] [inst_9 : Algebra K L] [inst_10 : Algebra A L]
  [inst_11 : IsScalarTower A K L] [inst_12 : IsScalarTower A B L] [IsIntegrallyClosed A]
  [inst_14 : IsIntegralClosure B A L] [FiniteDimensional K L] [h : IsGalois K L], Algebra.IsInvariant A B Gal(L/K)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the first morphism of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.mor₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → (self : CategoryTheory.Pretriangulated.Triangle C) → self.obj₁ ⟶ self.obj₂
-- Mathlib.Probability.BrownianMotion.Basic
/-- A centered Gaussian process with the right covariance is a pre-Brownian motion.  -/
ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covariance : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsGaussianProcess X P →
    (∀ (t : NNReal), ∫ (x : Ω), X t x ∂P = 0) →
      (∀ (s t : NNReal), s ≤ t → ProbabilityTheory.covariance (X s) (X t) P = ↑s) →
        ProbabilityTheory.IsPreBrownianReal X P
-- Mathlib.Order.Bounds.Basic
isLUB_Iio : ∀ {γ : Type u_3} [inst : LinearOrder γ] [DenselyOrdered γ] {a : γ}, IsLUB (Set.Iio a) a
-- Mathlib.Order.Filter.Interval
Filter.tendsto_uIcc_of_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l],
  Filter.TendstoIxxClass Set.uIcc l l
-- Mathlib.Data.Ineq
/-- Given an expression `e`, parse it as a `=`, `≤` or `<`, or the negation of such, and return this
relation (as a `Linarith.Ineq`) together with the type in which the (in)equality occurs, the two
sides of the (in)equality, and a Boolean flag indicating the presence or absence of the `¬`.

This function is more naturally in the `Option` monad, but it is convenient to put in `MetaM`
for compositionality.
 -/
Lean.Expr.ineqOrNotIneq? : Lean.Expr → Lean.MetaM (Bool × Mathlib.Ineq × Lean.Expr × Lean.Expr × Lean.Expr)
-- Init.Data.Array.Lemmas
Array.getElem_extract_aux : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {start stop : ℕ}, i < (xs.extract start stop).size → start + i < xs.size
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If a `J`-shaped diagram in `FullSubcategory P` has a limit cone in `C` whose cone point lives
in the full subcategory, then this defines a limit in the full subcategory.  -/
CategoryTheory.Limits.createsLimitFullSubcategoryInclusion' : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {P : CategoryTheory.ObjectProperty C} →
          (F : CategoryTheory.Functor J P.FullSubcategory) →
            {c : CategoryTheory.Limits.Cone (F.comp P.ι)} →
              CategoryTheory.Limits.IsLimit c → P c.pt → CategoryTheory.CreatesLimit F P.ι
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonJsonNumber : Lean.ToJson Lean.JsonNumber
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.mem_nonunits_iff_of_ne_zero : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : GroupWithZero α] [inst_2 : SubmonoidClass C α] {S : C}
  {a : ↥S}, ↑a ≠ 0 → (a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_lt_map_iff_of_injective : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → ∀ {H K : Subgroup G}, Subgroup.map f H < Subgroup.map f K ↔ H < K
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a : α} {v : β},
  (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
-- Lean.Setup
/-- Plugins to initialize with the module.  -/
Lean.ModuleSetup.plugins : Lean.ModuleSetup → Array Lean.Plugin
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRat.inj : ∀ {β : Type u} {α : Type v} {id : ℕ} {c : β} {pivot : Std.Sat.Literal α} {rupHints : Array ℕ}
  {ratHints : Array (ℕ × Array ℕ)} {id_1 : ℕ} {c_1 : β} {pivot_1 : Std.Sat.Literal α} {rupHints_1 : Array ℕ}
  {ratHints_1 : Array (ℕ × Array ℕ)},
  Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints =
      Std.Tactic.BVDecide.LRAT.Action.addRat id_1 c_1 pivot_1 rupHints_1 ratHints_1 →
    id = id_1 ∧ c = c_1 ∧ pivot = pivot_1 ∧ rupHints = rupHints_1 ∧ ratHints = ratHints_1
-- Mathlib.Data.Ordmap.Invariants
cmpLE.congr_simp : ∀ {α : Type u_3} [inst : LE α] {inst_1 : DecidableLE α} [inst_2 : DecidableLE α] (x x_1 : α),
  x = x_1 → ∀ (y y_1 : α), y = y_1 → cmpLE x y = cmpLE x_1 y_1
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
uliftPowersHom_apply_apply : ∀ (M : Type u) [inst : Monoid M] (a : M) (x : ULift.{u, 0} (Multiplicative ℕ)),
  ((uliftPowersHom M) a) x = a ^ Multiplicative.toAdd (MulEquiv.ulift x)
-- Mathlib.RingTheory.Flat.Equalizer
/-- Given a short exact sequence `0 → M → N → P → 0` with `P` flat,
then any `A ⊗ M → A ⊗ N` is injective.
 -/
LinearMap.lTensor_injective_of_exact_of_flat : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_4}
  {P : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R N] [inst_6 : Module R P]
  [Module.Flat R P] (f : N →ₗ[R] P),
  Function.Surjective ⇑f →
    ∀ (g : M →ₗ[R] N),
      Function.Injective ⇑g →
        Function.Exact ⇑g ⇑f →
          ∀ (A : Type u_6) [inst_8 : AddCommGroup A] [inst_9 : Module R A], Function.Injective ⇑(LinearMap.lTensor A g)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_eq_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α}, σ.cycleType = 0 ↔ σ = 1
-- Mathlib.NumberTheory.Real.Irrational
irrational_natCast_mul_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.diseq_cancel_var : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (c : ℤ)
  (x : Lean.Grind.CommRing.Var) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.cancel_var_cert c x p₁ p₂ = true →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx p₁ ≠ 0 → Lean.Grind.CommRing.Poly.denote ctx p₂ ≠ 0
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.num.injEq : ∀ (v v_1 : ℕ), (Lean.IR.LitVal.num v = Lean.IR.LitVal.num v_1) = (v = v_1)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_surjective : Function.Surjective Real.log
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.intervalIntegrable_charFun : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {a b : ℝ},
  IntervalIntegrable (MeasureTheory.charFun μ) MeasureTheory.volume a b
-- Std.Data.TreeMap.Raw.Basic
/-- Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map.
 -/
Std.TreeMap.Raw.union : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀}
  {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} (self : data.SieveStruct f g),
  CategoryTheory.CategoryStruct.comp self.q (data.f self.i₀) = CategoryTheory.CategoryStruct.comp (F.map g) f
-- Std.Async.System
/-- Gets all environment variables.
 -/
Std.Async.System.getEnv : IO Std.Async.System.Environment
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItem.textEdit? : Lean.Lsp.ResolvableCompletionItem → Option Lean.Lsp.InsertReplaceEdit
-- Std.Time.Date.Unit.Month
Std.Time.Month.instDecidableLeOrdinal : {x y : Std.Time.Month.Ordinal} → Decidable (x ≤ y)
-- Mathlib.Topology.Bases
FirstCountableTopology.mk : ∀ {α : Type u} [t : TopologicalSpace α], (∀ (a : α), (nhds a).IsCountablyGenerated) → FirstCountableTopology α
-- Mathlib.Topology.Homotopy.Lifting
Path.Homotopic.Quotient.cast.hcongr_9 : ∀ (X X' : Type u),
  X = X' →
    ∀ (inst : TopologicalSpace X) (inst' : TopologicalSpace X'),
      inst ≍ inst' →
        ∀ (x : X) (x' : X'),
          x ≍ x' →
            ∀ (y : X) (y' : X'),
              y ≍ y' →
                ∀ (γ : Path.Homotopic.Quotient x y) (γ' : Path.Homotopic.Quotient x' y'),
                  γ ≍ γ' →
                    ∀ (x'_1 : X) (x'' : X'),
                      x'_1 ≍ x'' →
                        ∀ (y'_1 : X) (y'' : X'),
                          y'_1 ≍ y'' →
                            ∀ (hx : x'_1 = x) (hx' : x'' = x'),
                              hx ≍ hx' → ∀ (hy : y'_1 = y) (hy' : y'' = y'), hy ≍ hy' → γ.cast hx hy ≍ γ'.cast hx' hy'
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is
automatically continuous.  -/
LinearMap.continuous_of_nonzero_on_open : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜) (s : Set E),
  IsOpen s → s.Nonempty → (∀ x ∈ s, l x ≠ 0) → Continuous ⇑l
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt32 = Int32.ofInt n
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.hom_ofHom : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (f : X →ₙ+ Y),
  AddSemigrp.Hom.hom (AddSemigrp.ofHom f) = f
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.toMLList.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 α) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (s' : Stream'.Seq α) → motive (some (a, s'))),
  (match none with
    | none => h_1 ()
    | some (a, s') => h_2 a s') =
    h_1 ()
-- Init.PropLemmas
exists₂_imp : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop} {P : (x : α) → p x → Prop},
  (∃ x, ∃ (h : p x), P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The coproduct cocone associated to the explicit finite coproduct.  -/
CompHausLike.finiteCoproduct.cofan : {P : TopCat → Prop} →
  {α : Type w} →
    [Finite α] → (X : α → CompHausLike P) → [CompHausLike.HasExplicitFiniteCoproduct X] → CategoryTheory.Limits.Cofan X
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.Position.mk.sizeOf_spec : ∀ (line character : ℕ), sizeOf { line := line, character := character } = 1 + sizeOf line + sizeOf character
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.toArray.eq_1 : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (m : Std.HashSet α), m.toArray = m.inner.keysArray
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.eval_nil : ∀ {α : Type u_1} (a : α → Bool), Std.Sat.CNF.Clause.eval a [] = false
-- Mathlib.GroupTheory.Complement
AddSubgroup.LeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.LeftTransversal = { S // AddSubgroup.IsComplement S ↑H }
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If the pairwise pullbacks exist, this is the pre-`1`-hypercover where the covers
by the pullbacks are given by the pullbacks themselves.  -/
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} → (E : J.ZeroHypercover S) → [E.HasPullbacks] → J.toGrothendieck.OneHypercover S
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- If one controls the enorm of every `f x`, then one controls the enorm of `f`.  -/
ContinuousLinearMap.opENorm_le_bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {M : ENNReal}, (∀ (x : E), ‖f x‖ₑ ≤ M * ‖x‖ₑ) → ‖f‖ₑ ≤ M
-- Std.Time.Zoned.ZoneRules
/-- Represents types of wall clocks or standard times.
 -/
Std.Time.TimeZone.StdWall : Type
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_mapM : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.mapM f it) =
    Std.Iter.foldM
      (fun d b => do
        let c ← f b
        pure (g d c))
      init it
-- Mathlib.Data.ULift
PLift.exists : ∀ {α : Sort u} {p : PLift α → Prop}, (∃ x, p x) ↔ ∃ x, p { down := x }
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.ext_iff : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] {f g : IncidenceAlgebra 𝕜 α},
  f = g ↔ ∀ (a b : α), a ≤ b → f a b = g a b
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.of_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Function.Bijective ⇑(algebraMap R S) → Algebra.IsStandardOpenImmersion R S
-- Lean.DocString.Parser
/-- Parses an unordered list.  -/
Lean.Doc.Parser.unorderedList : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Order.Monotone.Monovary
Monovary.eq_1 : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (g : ι → β),
  Monovary f g = ∀ ⦃i j : ι⦄, g i < g j → f i ≤ f j
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.Functor.sieves_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ),
  (CategoryTheory.Functor.sieves C).obj X = CategoryTheory.Sieve (Opposite.unop X)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toLp.congr_simp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [inst_5 : OpensMeasurableSpace E]
  [inst_6 : SecondCountableTopologyEither E F] (f f_1 : SchwartzMap E F),
  f = f_1 → ∀ (p : ENNReal) (μ : MeasureTheory.Measure E) [hμ : μ.HasTemperateGrowth], f.toLp p μ = f_1.toLp p μ
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instLineDerivSMulTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F],
  LineDerivSMul 𝕜 E (TestFunction Ω F ⊤) (TestFunction Ω F ⊤)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.instCoeSort : CoeSort FintypeCat (Type u_1)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The current label to run (or `none` for the halting state)  -/
Turing.TM2.Cfg.l : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Cfg Γ Λ σ → Option Λ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).isEmpty = false →
    ((Std.DTreeMap.Const.alter t k f).minKey! = k ↔
      (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Init.Data.Array.Find
Array.find?_replicate_eq_some_iff : ∀ {α : Type u_1} {n : ℕ} {a b : α} {p : α → Bool},
  Array.find? p (Array.replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.splitter : {α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m γ) → Sort u_3) →
      (it₂ : Option (Std.IterM m γ)) → (Unit → motive none) → ((it₂ : Std.IterM m γ) → motive (some it₂)) → motive it₂
-- Mathlib.Data.ENat.Pow
ENat.zero_epow : ∀ {y : ℕ∞}, y ≠ 0 → 0 ^ y = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_alter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β}
  {hc : k' ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey k' hc =
    if heq : compare k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Algebra.Group.Equiv.Opposite
MulHom.unop.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N], MulHom.unop = MulHom.op.symm
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.skeletal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α), CategoryTheory.Skeletal C
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_counitIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S)
  (X_1 : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).counitIso.hom.app X_1).f =
    CategoryTheory.CategoryStruct.id X_1.A
-- Init.Data.String.Defs
String.Slice.Pos.ext : ∀ {s : String.Slice} {x y : s.Pos}, x.offset = y.offset → x = y
-- Init.Data.Rat.Lemmas
Rat.instAssociativeHAdd : Std.Associative fun x1 x2 => x1 + x2
-- Lean.Meta.SizeOf
/-- Convert a recursor application into a `_sizeOf_<idx>` application.  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.SizeOfSpecNested.recToSizeOf : Lean.Expr → Lean.Meta.SizeOfSpecNested.M Lean.Expr
-- Lean.Data.Format
Lean.instToFormatName_lean : Std.ToFormat Lean.Name
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.State.expectedType? : Lean.Elab.Term.ElabAppArgs.State → Option Lean.Expr
-- Init.Data.UInt.Lemmas
UInt32.ofFin_le_iff_le : ∀ {a b : Fin UInt32.size}, UInt32.ofFin a ≤ UInt32.ofFin b ↔ a ≤ b
-- Mathlib.Data.Finset.Lattice.Fold
Finset.lt_inf_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α} {a : α},
  a < ⊤ → (a < s.inf f ↔ ∀ b ∈ s, a < f b)
-- Mathlib.Data.Option.NAry
/-- Symmetric statement to `Option.map_map₂_right_anticomm`.  -/
Option.map_map₂_antidistrib_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {α' : Type u_5} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' b (g' a)) → Option.map g (Option.map₂ f a b) = Option.map₂ f' b (Option.map g' a)
-- Std.Time.DateTime.WallTime
Std.Time.instReprWallTime_1 : Repr Std.Time.WallTime
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.forget_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C C)
  (A : CategoryTheory.Endofunctor.Algebra F), (CategoryTheory.Endofunctor.Algebra.forget F).obj A = A.a
-- Lean.Parser.Command
Lean.Parser.Command.structureTk.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_neg : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommGroup P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P] [inst_6 : Module R Q]
  (f : N →ₗ[R] P), LinearMap.rTensor Q (-f) = -LinearMap.rTensor Q f
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.uppcRec.match_1.eq_1 : ∀ {w : ℕ} (motive : (s : ℕ) → s < w → Sort u_1) (hs : 0 < w) (h_1 : (hs : 0 < w) → motive 0 hs)
  (h_2 : (i : ℕ) → (hs : i + 1 < w) → motive i.succ hs),
  (match 0, hs with
    | 0, hs => h_1 hs
    | i.succ, hs => h_2 i hs) =
    h_1 hs
-- Mathlib.Logic.Function.Basic
Function.Involutive.eq_1 : ∀ {α : Sort u_1} (f : α → α), Function.Involutive f = ∀ (x : α), f (f x) = x