mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_3 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hrb_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced) (size : ℕ) (rk : α)
  (rv : β rk) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r_3 : Std.DTreeMap.Internal.Impl α β)
  (hrb_4 :
    (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r_3)).Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
      (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r_3)).size
      Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner size rk rv Std.DTreeMap.Internal.Impl.leaf
        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r_3))
      hrb_2 hrb_4 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner 3 rk rv
      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r_3)
-- Init.WFExtrinsicFix
/-- The function implemented as the loop
`opaqueFix₃ R F a b c = F a b c (fun a' b' c' _ => opaqueFix₃ R F a' b' c')`.
`opaqueFix₃ R F` is the fixpoint of the functional `F`, as long as the loop is
well-founded.

The loop might run forever depending on `F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
 -/
WellFounded.opaqueFix₃ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {γ : (a : α) → β a → Sort u_3} →
      {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4} →
        [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] →
          (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) →
            ((a : α) →
                (b : β a) →
                  (c : γ a b) →
                    ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c) →
              (a : α) → (b : β a) → (c : γ a b) → C₃ a b c
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (φ₃ : K₃ ⟶ L₃) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) (a' : K₂ ⟶ K₃)
  (b' : L₂ ⟶ L₃) (comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃)
  {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone φ₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a')
        (CategoryTheory.CategoryStruct.comp b b') ⋯)
      h =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm') h)
-- Init.Prelude
/-- The homogeneous version of `HAndThen`: `a >> b : α` where `a b : α`.
Because `b` is "lazy" in this notation, it is passed as `Unit → α` to the
implementation so it can decide when to evaluate it.
 -/
AndThen : Type u → Type u
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] (f : Γ₀ →*₀ Γ'₀) (hf : Monotone ⇑f) (v : Valuation R Γ₀) (r : R),
  (Valuation.map f hf v) r = f (v r)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.symm_continuousWithinAt_comp_right_iff : ∀ {𝕜 : 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) {X : Type u_4}
  [inst_4 : TopologicalSpace X] {f : H → X} {s : Set H} {x : H},
  ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x) ↔ ContinuousWithinAt f s x
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Polynomial.contentIdeal_one : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.contentIdeal 1 = ⊤
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyGE?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky v l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGE?.go k (some ky) l
      | Ordering.eq => some ky
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyGE?.go k best r
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeftObjCompIso_inv_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D')
  (X : CategoryTheory.Functor D' E) (X_1 : C),
  ((F.whiskeringLeftObjCompIso G).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj (G.obj (F.obj X_1)))
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.top_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C), ⊤.obj.left = X
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Composition of two `AffineEquiv`alences, applied left to right.  -/
AffineEquiv.trans : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {P₃ : Type u_4} →
        {V₁ : Type u_6} →
          {V₂ : Type u_7} →
            {V₃ : Type u_8} →
              [inst : Ring k] →
                [inst_1 : AddCommGroup V₁] →
                  [inst_2 : AddCommGroup V₂] →
                    [inst_3 : AddCommGroup V₃] →
                      [inst_4 : Module k V₁] →
                        [inst_5 : Module k V₂] →
                          [inst_6 : Module k V₃] →
                            [inst_7 : AddTorsor V₁ P₁] →
                              [inst_8 : AddTorsor V₂ P₂] →
                                [inst_9 : AddTorsor V₃ P₃] → (P₁ ≃ᵃ[k] P₂) → (P₂ ≃ᵃ[k] P₃) → P₁ ≃ᵃ[k] P₃
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_infs : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] {s t : Finset α} {a : α} [inst_2 : DecidableLE α]
  [inst_3 : BoundedOrder α],
  a ∈ lowerClosure ↑s → a ∈ lowerClosure ↑t → (s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a
-- Lean.Expr
/-- Projection-expressions. They are redundant, but are used to create more compact
terms, speed up reduction, and implement eta for structures.
The type of `struct` must be a one-constructor inductive type.
If `I.mk` is the constructor of an `m`-parameter inductive type `I`,
then ``.proj `I k (@I.mk p1 ... pm f0 f1 ...)`` is definitionally equal to `fk`.

The kernel and elaborator check whether the `typeName` matches the type of `struct`,
whether the zero-based index is valid (it must be smaller than the number of constructor fields),
and whether the projection itself is valid (for inductive predicates, the fields must be propositions).
When exporting Lean developments to other systems, `proj` can be replaced with `typeName.rec`
applications.
Non-recursive structures (one-constructor inductive types with no indices) have an eta rule:
if `e : I p1 ... pm`, then `e` and `@I.mk p1 ... pm e.1 e.2 ... e.n` are definitionally equal.

Example, given `a : Nat × Bool`, `a.1` is represented as
```
.proj `Prod 0 a
```
and `a` is definitionally equal to `@Prod.mk Nat Bool a.1 a.2` by the structure eta rule.
 -/
Lean.Expr.proj : Lean.Name → ℕ → Lean.Expr → Lean.Expr
-- Init.Data.Iterators.Basic
/-- Internal implementation detail of the iterator.  -/
Std.IterM.internalState : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → α
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.noConfusionType : Sort v✝ → Lean.JsonRpc.MessageKind → Lean.JsonRpc.MessageKind → Sort v✝
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeEmpty : {α : Type u} → Fintype ↑∅
-- Lean.Elab.Tactic.SolveByElim
/-- Parse the `using ...` argument for `solve_by_elim`.  -/
Lean.Elab.Tactic.SolveByElim.parseUsing : Option (Lean.TSyntax `Lean.Parser.Tactic.SolveByElim.using_) → Array Lean.Ident
-- Mathlib.CategoryTheory.MorphismProperty.Descent
/-- If `P` descends along `Q`, then `P.diagonal` descends along `Q`.  -/
CategoryTheory.MorphismProperty.instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (P Q : CategoryTheory.MorphismProperty C) [P.DescendsAlong Q] [P.RespectsIso] [Q.IsStableUnderBaseChange],
  P.diagonal.DescendsAlong Q
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonCompletionItemCapabilities.toJson : Lean.Lsp.CompletionItemCapabilities → Lean.Json
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.tail.aux.match_1.splitter : {α : Type u_1} →
  (motive : Option (α × Stream'.WSeq α) → Sort u_2) →
    (x : Option (α × Stream'.WSeq α)) →
      (Unit → motive none) → ((fst : α) → (s : Stream'.WSeq α) → motive (some (fst, s))) → motive x
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.op_apply_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] (f : α ≃* β) (a : βᵐᵒᵖ),
  (MulEquiv.op f).symm a = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a
-- Mathlib.Algebra.Lie.Basic
LieEquiv.toLinearEquiv_mk : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁)
  (h₁ : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun),
  { toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toLinearEquiv =
    { toLinearMap := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }
-- Mathlib.RingTheory.Artinian.Module
isArtinian_finsupp : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [Finite ι] [IsArtinian R M], IsArtinian R (ι →₀ M)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.mono_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U₁ U₂ V : Submodule 𝕜 E}, U₂ ≤ U₁ → U₁ ⟂ V → U₂ ⟂ V
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.BinaryTree.toOrdNode.match_1.eq_1 : ∀ {α : Type u_1} (motive : BinaryTree α → Sort u_2) (h_1 : Unit → motive BinaryTree.nil)
  (h_2 : (x : α) → (l r : BinaryTree α) → motive (BinaryTree.node x l r)),
  (match BinaryTree.nil with
    | BinaryTree.nil => h_1 ()
    | BinaryTree.node x l r => h_2 x l r) =
    h_1 ()
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.usedNames : Lean.Elab.Term.CollectPatternVars.Context → Std.HashSet Lean.Name
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.GrothendieckTopology.OneHypercover.instIsPreservedById : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (E : J.OneHypercover X), E.IsPreservedBy (CategoryTheory.Functor.id C) J
-- Mathlib.Algebra.Algebra.Equiv
/-- **Alias** of `AlgEquiv.toAlgHom_ofAlgHom`. -/
AlgEquiv.coe_algHom_ofAlgHom : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
  (h₂ : g.comp f = AlgHom.id R A₁), ↑(AlgEquiv.ofAlgHom f g h₁ h₂) = f
-- Aesop.Rule.Basic
Aesop.Rule.compareByPriorityThenName : {α : Type} → [Ord α] → Aesop.Rule α → Aesop.Rule α → Ordering
-- Init.Data.Array.TakeDrop
List.exists_of_set : ∀ {α : Type u_1} {i : ℕ} {a' : α} {l : List α} (h : i < l.length),
  ∃ l₁ l₂, l = l₁ ++ l[i] :: l₂ ∧ l₁.length = i ∧ l.set i a' = l₁ ++ a' :: l₂
-- Mathlib.Data.PFun
Part.Mem.eq_1 : ∀ {α : Type u_1} (o : Part α) (a : α), o.Mem a = ∃ (h : o.Dom), o.get h = a
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_6 : ∀ (k : ℕ) (cf cg : Nat.Partrec.Code),
  Nat.Partrec.Code.evaln k.succ (cf.pair cg) = fun n => do
    guard (n ≤ k)
    Nat.pair <$> Nat.Partrec.Code.evaln (k + 1) cf n <*> Nat.Partrec.Code.evaln (k + 1) cg n
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.sup_univ_eq_ciSup : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] [inst_1 : Fintype ι] (f : ι → α),
  Finset.univ.sup f = ⨆ i, f i
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.ext_inner_left_basis : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} {x y : E} (b : Module.Basis ι 𝕜 E), (∀ (i : ι), inner 𝕜 (b i) x = inner 𝕜 (b i) y) → x = y
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ofSigmaCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.R),
  (CategoryTheory.Limits.Multicofork.ofSigmaCofork a).π i = CategoryTheory.CategoryStruct.comp (d.inj i) a.π
-- Mathlib.Data.Nat.Pairing
/-- Unpairing function for the natural numbers.  -/
Nat.unpair : ℕ → ℕ × ℕ
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ◫ θ`.  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp : (Type → Type) → Type
-- Mathlib.Data.Finset.Sups
Finset.infs_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ⊼ t₁ ⊆ s₂ ⊼ t₂
-- Mathlib.Topology.Irreducible
IsPreirreducible.preimage_of_isPreirreducible_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {V : Set Y},
  IsPreirreducible V →
    ∀ (f : X → Y), IsOpenMap f → (∀ (x : Y), IsPreirreducible (f ⁻¹' {x})) → IsPreirreducible (f ⁻¹' V)
-- Mathlib.Probability.Decision.Risk.Basic
ProbabilityTheory.bayesRisk_le_minimaxRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (π : MeasureTheory.Measure Θ)
  [MeasureTheory.IsProbabilityMeasure π], ProbabilityTheory.bayesRisk ℓ P π ≤ ProbabilityTheory.minimaxRisk ℓ P
-- Lean.Environment
/-- Data structure holding a sequence of `AsyncConst`s optimized for efficient access.  -/
_private.Lean.Environment.0.Lean.AsyncConsts : Type
-- Mathlib.RingTheory.Ideal.Basic
/-- `Πᵢ Iᵢ` as an ideal of `Πᵢ Rᵢ`.  -/
Ideal.pi : {ι : Type u_1} →
  {R : ι → Type u_5} → [inst : (i : ι) → Semiring (R i)] → ((i : ι) → Ideal (R i)) → Ideal ((i : ι) → R i)
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getUInt64Value? : Lean.Expr → OptionT Id UInt64
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.isStrongGenerator_iff_exists_extremalEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P],
  P.IsStrongGenerator ↔ ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.ExtremalEpi p
-- Mathlib.RingTheory.Algebraic.Integral
/-- This used to be an `alias` of `Algebra.isAlgebraic_iff_isIntegral` but that would make
`Algebra.IsAlgebraic K A` an explicit parameter instead of instance implicit.  -/
Algebra.IsAlgebraic.isIntegral : ∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] [Algebra.IsAlgebraic K A],
  Algebra.IsIntegral K A
-- Mathlib.Tactic.Linter.EmptyLine
/-- If a file contains one of these names as segments, we disable the `emptyLine` linter.  -/
Mathlib.Linter.EmptyLine.SkippedFileSegments : Std.HashSet Lean.Name
-- Aesop.EMap
/-- The mappings stored in the map. Defeq expressions are identified, so
for each equivalence class of defeq expressions we only store one
representative. Missing values indicate expressions that were removed from the
map.  -/
Aesop.EMap.rep : {α : Type u_1} → Aesop.EMap α → Lean.PArray (Option (Lean.Expr × α))
-- Lean.Data.Name
Lean.Name.isNum : Lean.Name → Bool
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
/-- Write `n = p ^ (k + 1) * m` where the prime `p` does not divide `m`, then the inertia degree of
`p` in `ℚ(ζₙ)` is the order of `p` modulo `m`.
 -/
IsCyclotomicExtension.Rat.inertiaDegIn_eq : ∀ (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [IsCyclotomicExtension {n} ℚ K],
  n = p ^ (k + 1) * m → ¬p ∣ m → (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p
-- Aesop.BuiltinRules
Aesop.BuiltinRules.not_intro : ∀ {P : Prop}, (P → False) → ¬P
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk : {Γ : Type u_1} → [inst : Inhabited Γ] → Γ → Turing.ListBlank Γ → Turing.ListBlank Γ → Turing.Tape Γ
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The right part of the Dyck word decomposition,
outside the `U, D` pair that `firstReturn` refers to. `outsidePart 0 = 0`.  -/
DyckWord.outsidePart : DyckWord → DyckWord
-- Init.Data.UInt.Bitwise
UInt32.ofNat_xor : ∀ (a b : ℕ), UInt32.ofNat (a ^^^ b) = UInt32.ofNat a ^^^ UInt32.ofNat b
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instNatCast : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → NatCast (DoubleCentralizer 𝕜 A)
-- Mathlib.Probability.IdentDistrib
/-- This lemma is superseded by `MemLp.uniformIntegrable_of_identDistrib` which only requires
`AEStronglyMeasurable`.  -/
ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib_aux : ∀ {α : Type u_1} [inst : MeasurableSpace α] {E : Type u_5} [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [BorelSpace E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_6} {f : ι → α → E} {j : ι}
  {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      MeasureTheory.MemLp (f j) p μ →
        (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
          (∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ) → MeasureTheory.UniformIntegrable f p μ
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst : ∀ {X Y S : Type v} {f : X ⟶ S} {g : Y ⟶ S} {c : CategoryTheory.Limits.PullbackCone f g}
  (hc : CategoryTheory.Limits.IsLimit c) (x : c.pt),
  (↑((CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj hc) x)).1 =
    (CategoryTheory.ConcreteCategory.hom c.fst) x
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommSemiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p₁.mul p₂) =
        Lean.Grind.CommRing.Poly.denoteS ctx p₁ * Lean.Grind.CommRing.Poly.denoteS ctx p₂
-- Batteries.Data.Float.Rat
Rat.instCoeFloat_batteries : Coe ℚ Float
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.conjugator.cons_append : ∀ {α : Type u} [inst : DecidableEq α] {a b : α × Bool} (L : List (α × Bool)),
  FreeGroup.reduceCyclically.conjugator (a :: (L ++ [b])) =
    if b.1 = a.1 ∧ (!b.2) = a.2 then a :: FreeGroup.reduceCyclically.conjugator L else []
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_3 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_3 l b
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
Pi.spanSubset.congr_simp : ∀ (R : Type u_2) {η : Type u_4} [inst : Semiring R] [inst_1 : Finite η] (s s_1 : Set η),
  s = s_1 → Pi.spanSubset R s = Pi.spanSubset R s_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {a : α} {fallback : β},
  Std.DTreeMap.Const.getD ∅ a fallback = fallback
-- Mathlib.Data.Finsupp.MonomialOrder
/-- **Alias** of `MonomialOrder.addCommMonoidSyn`.

---

`syn` is an additive commutative monoid  -/
MonomialOrder.acm : {σ : Type u_1} → (self : MonomialOrder σ) → AddCommMonoid self.syn
-- Mathlib.Topology.Homotopy.Path
/-- Cast a path homotopy class using equalities of endpoints.  -/
Path.Homotopic.Quotient.cast : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x y : X} → Path.Homotopic.Quotient x y → {x' y' : X} → x' = x → y' = y → Path.Homotopic.Quotient x' y'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.SemiCartesianMonoidalCategory.snd Y X) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X Y
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.toFinset_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : VSub α β] (s t : Set β) [inst_2 : Fintype ↑s]
  [inst_3 : Fintype ↑t] [inst_4 : Fintype ↑(s -ᵥ t)], (s -ᵥ t).toFinset = s.toFinset -ᵥ t.toFinset
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerToAddOpposite_apply_coe : ∀ {M : Type u_2} [inst : AddZeroClass M] (r : ↥(AddSubsemigroup.center M)),
  ↑(AddSubmonoid.centerToAddOpposite r) = AddOpposite.op ↑r