mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Command
Lean.Elab.Command.State.mk.inj : ∀ {env : Lean.Environment} {messages : Lean.MessageLog} {scopes : List Lean.Elab.Command.Scope}
  {usedQuotCtxts : Lean.NameSet} {nextMacroScope maxRecDepth : ℕ} {ngen : Lean.NameGenerator}
  {auxDeclNGen : Lean.DeclNameGenerator} {infoState : Lean.Elab.InfoState} {traceState : Lean.TraceState}
  {snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)} {env_1 : Lean.Environment}
  {messages_1 : Lean.MessageLog} {scopes_1 : List Lean.Elab.Command.Scope} {usedQuotCtxts_1 : Lean.NameSet}
  {nextMacroScope_1 maxRecDepth_1 : ℕ} {ngen_1 : Lean.NameGenerator} {auxDeclNGen_1 : Lean.DeclNameGenerator}
  {infoState_1 : Lean.Elab.InfoState} {traceState_1 : Lean.TraceState}
  {snapshotTasks_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { env := env, messages := messages, scopes := scopes, usedQuotCtxts := usedQuotCtxts,
        nextMacroScope := nextMacroScope, maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
        infoState := infoState, traceState := traceState, snapshotTasks := snapshotTasks } =
      { env := env_1, messages := messages_1, scopes := scopes_1, usedQuotCtxts := usedQuotCtxts_1,
        nextMacroScope := nextMacroScope_1, maxRecDepth := maxRecDepth_1, ngen := ngen_1, auxDeclNGen := auxDeclNGen_1,
        infoState := infoState_1, traceState := traceState_1, snapshotTasks := snapshotTasks_1 } →
    env = env_1 ∧
      messages = messages_1 ∧
        scopes = scopes_1 ∧
          usedQuotCtxts = usedQuotCtxts_1 ∧
            nextMacroScope = nextMacroScope_1 ∧
              maxRecDepth = maxRecDepth_1 ∧
                ngen = ngen_1 ∧
                  auxDeclNGen = auxDeclNGen_1 ∧
                    infoState = infoState_1 ∧ traceState = traceState_1 ∧ snapshotTasks = snapshotTasks_1
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.mk_eq_one_iff_sub_mem : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] (x : R), (Ideal.Quotient.mk I) x = 1 ↔ x - 1 ∈ I
-- Init.System.IO
IO.FS.instBEqSystemTime.beq : IO.FS.SystemTime → IO.FS.SystemTime → Bool
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- A version of `convexBodyLT` with an additional condition at a fixed complex place. This is
needed to ensure the element constructed is not real, see for example
`exists_primitive_element_lt_of_isComplex`.
 -/
NumberField.mixedEmbedding.convexBodyLT' : (K : Type u_1) →
  [inst : Field K] →
    (NumberField.InfinitePlace K → NNReal) → { w // w.IsComplex } → Set (NumberField.mixedEmbedding.mixedSpace K)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_ext : ∀ {M N : SemiNormedGrp₁} {f g : M ⟶ N}, SemiNormedGrp₁.Hom.hom f = SemiNormedGrp₁.Hom.hom g → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.lt : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper] (x : ↑P.II), ↑x < ↑(P.p x)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} (self : F.DescentDataAsCoalgebra f) (i₁ i₂ i₃ : ι),
  CategoryTheory.CategoryStruct.comp (self.hom i₁ i₂)
      ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (self.hom i₂ i₃))) =
    CategoryTheory.CategoryStruct.comp (self.hom i₁ i₃)
      ((F.map (f i₁).op.toLoc).l.toFunctor.map
        ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (self.obj i₃))))
-- Mathlib.Data.Seq.Computation
/-- Flatten a computation of computations into a single computation.  -/
Computation.join : {α : Type u} → Computation (Computation α) → Computation α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingParallelPair.instNonemptyStructuredArrowWalkingReflexivePairInclusionWalkingReflexivePair : ∀ (X : CategoryTheory.Limits.WalkingReflexivePair),
  Nonempty (CategoryTheory.StructuredArrow X CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair)
-- Mathlib.Data.Finsupp.Basic
/-- `subtypeDomain` but as an `AddMonoidHom`.  -/
Finsupp.subtypeDomainAddMonoidHom : {α : Type u_1} → {M : Type u_5} → [inst : AddZeroClass M] → {p : α → Prop} → (α →₀ M) →+ Subtype p →₀ M
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonFunctor.eq_1 : ∀ (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],
  CategoryTheory.Functor.mapAddMonFunctor C D =
    { obj := fun F => F.mapAddMon,
      map := fun {X Y} α => { app := fun A => CategoryTheory.AddMon.Hom.mk' (α.hom.app A.X) ⋯ ⋯, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The morphism `A ⟶ H` induced by a morphism `k : A ⟶ Q` such that `k ≫ g' = 0`  -/
CategoryTheory.ShortComplex.RightHomologyData.liftH : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (h : S.RightHomologyData) → {A : C} → (k : A ⟶ h.Q) → CategoryTheory.CategoryStruct.comp k h.g' = 0 → (A ⟶ h.H)
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_sdiff_singleton_zero : ∀ {M : Type u_1} [inst : AddZeroClass M] (s : Set M), AddSubmonoid.closure (s \ {0}) = AddSubmonoid.closure s
-- Mathlib.Analysis.Calculus.Deriv.Add
HasStrictDerivAt.const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (c : F),
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => c - f x) (-f') x
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_prod_range_succ₀ : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ℕ → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ℕ), AEMeasurable (f i) μ) → ∀ (n : ℕ), ProbabilityTheory.IndepFun (∏ j ∈ Finset.range n, f j) (f n) μ
-- Mathlib.Data.Finset.Insert
Finset.val_eq_singleton_iff : ∀ {α : Type u_1} {a : α} {s : Finset α}, s.val = {a} ↔ s = {a}
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.mergeSort.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_1 x
-- Std.Do.Triple.SpecLemmas
/-- The type of loop invariants used by the specifications of `for ... in ...` loops over string slices.
A loop invariant is a `PostCond` that takes as parameters

* A `String.Slice.Pos` representing the current position in the string slice `s`.
* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
  `let mut` variables and early return.
 -/
Std.Do.StringSliceInvariant : String.Slice → Type u → Std.Do.PostShape → Type u
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.denote_relabel : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {invert : Bool} (aig : Std.Sat.AIG α) (r : α → β) (start : ℕ) {hidx : start < (Std.Sat.AIG.relabel r aig).decls.size}
  (assign : β → Bool),
  ⟦assign, { aig := Std.Sat.AIG.relabel r aig, ref := { gate := start, invert := invert, hgate := hidx } }⟧ =
    ⟦assign ∘ r, { aig := aig, ref := { gate := start, invert := invert, hgate := ⋯ } }⟧
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f f_1 : X.src ⟶ Y.src) (e_f : f = f_1)
  (F F_1 : X.src ⨯ Y.tgt ⟶ X.tgt) (e_F : F = F_1)
  (le :
    (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj X.rel ≤
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
        Y.rel),
  { f := f, F := F, le := le } = { f := f_1, F := F_1, le := ⋯ }
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.startsWith_char_eq_head? : ∀ {c : Char} {s : String}, s.startsWith c = (s.toList.head? == some c)
-- Mathlib.Data.Finsupp.Basic
Finsupp.curry_uncurry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α →₀ β →₀ M), f.uncurry.curry = f
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.to_hasBasis : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s →
    (∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) → (∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') → l.HasBasis p' s'
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceAdditive : ∀ {α : Type u_1} [inst : Bornology α] [BoundedSpace α], BoundedSpace (Additive α)
-- Init.Data.Array.Lemmas
Array.mem_dite_empty_right : ∀ {α : Type u_1} {p : Prop} {x : α} [inst : Decidable p] {xs : p → Array α},
  (x ∈ if h : p then xs h else #[]) ↔ ∃ (h : p), x ∈ xs h
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The category of R-modules and their morphisms.

Note that in the case of `R = ℤ`, we cannot
impose here that the `ℤ`-multiplication field from the module structure is defeq to the one coming
from the `isAddCommGroup` structure (contrary to what we do for all module structures in
mathlib), which creates some difficulties down the road.  -/
ModuleCat : (R : Type u) → [Ring R] → Type (max u (v + 1))
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.biSup_measure_Iic : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Preorder α] {s : Set α},
  s.Countable → (∀ (x : α), ∃ y ∈ s, x ≤ y) → DirectedOn (fun x1 x2 => x1 ≤ x2) s → ⨆ x ∈ s, μ (Set.Iic x) = μ Set.univ
-- Aesop.Rule
Aesop.NormRuleInfo.mk : ℤ → Aesop.NormRuleInfo
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_mul : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ (t : ℝ), ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.Integrable (fun y => Real.exp (t * X y)) (κ ω')
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHMulInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.ContinuousMap.Algebra
Subalgebra.separatesPoints_monotone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : CommSemiring R] {A : Type u_3}
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A],
  Monotone fun s => s.SeparatesPoints
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.weakEquivalence_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.WeakEquivalence f ↔ HomotopicalAlgebra.weakEquivalences C f
-- Batteries.Data.List.Basic
/-- `findIdxs p l s` is the list of indexes of elements of `l` that satisfy `p`, added to an
optional parameter `s` (so that the members of `findIdxs p l s` will be greater than or
equal to `s` and less than `l.length + s`).   -/
List.findIdxs : {α : Type u_1} → (α → Bool) → List α → optParam ℕ 0 → List ℕ
-- Init.Data.SInt.Lemmas
Int16.ofInt_tdiv : ∀ {a b : ℤ},
  Int16.minValue.toInt ≤ a →
    a ≤ Int16.maxValue.toInt →
      Int16.minValue.toInt ≤ b → b ≤ Int16.maxValue.toInt → Int16.ofInt (a.tdiv b) = Int16.ofInt a / Int16.ofInt b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (Std.TreeMap.ofList l cmp).size = l.length
-- Mathlib.Logic.Relator
Relator.RightTotal.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop},
  (∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) →
    Relator.RightTotal r₁₂ → Relator.RightTotal r₂₃ → Relator.RightTotal r₁₃
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq : ∀ {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.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) (X : D) {Y₁ Y₂ : D}
  (f : Y₁ ⟶ Y₂),
  F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) =
    CategoryTheory.CategoryStruct.comp (self.μIso X Y₁).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (F.map f))
        (self.μIso X Y₂).hom)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
HasContDiffBump.out : ∀ {E : Type u_3} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} [self : HasContDiffBump E],
  Nonempty (ContDiffBumpBase E)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_zero_eq_singleton`. -/
Topology.CWComplex.openCell_zero_eq_singleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.openCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.monoOfLE_eq_iff : ∀ {X : SSet} [inst : X.Nonsingular] {x y : X.N} (h : x ≤ y) (g : { len := x.dim } ⟶ { len := y.dim })
  [CategoryTheory.Mono g],
  SSet.N.monoOfLE h = g ↔ (CategoryTheory.ConcreteCategory.hom (X.map g.op)) y.simplex = x.simplex
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.mul : Nat.Internal.SOM.Expr → Nat.Internal.SOM.Expr → Nat.Internal.SOM.Expr
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- Shifting cochain complexes by `n` and evaluating in a degree `i` identifies
to the evaluation in degree `i'` when `n + i = i'`.  -/
CochainComplex.shiftEval : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (n i i' : ℤ) →
        n + i = i' →
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).comp (HomologicalComplex.eval C (ComplexShape.up ℤ) i) ≅
            HomologicalComplex.eval C (ComplexShape.up ℤ) i')
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.uniqueToTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] → (P : C) → Unique (P ⟶ ⊤_ C)
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_not_piecewise : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M)
  (g : { a // ¬P a } →₀ M), Finsupp.subtypeDomain (fun x => ¬P x) (f.piecewise g) = g
-- Mathlib.Algebra.Ring.Basic
pred_ne_self : ∀ {α : Type u_3} [inst : NonAssocRing α] [Nontrivial α] (a : α), a - 1 ≠ a
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_finset_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  (a +ᵥ s).Nonempty ↔ s.Nonempty
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_root_pow : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) {n : ℕ}, n < f.natDegree → h.coeff (h.root ^ n) = Pi.single n 1
-- Lean.Expr
Lean.Expr.isBoolTrue : Lean.Expr → Bool
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorEqLocus_tmul : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f g : N →ₗ[R] P) (m : M) (x : ↥(f.eqLocus g)), ↑((LinearMap.tensorEqLocus S M f g) (m ⊗ₜ[R] x)) = m ⊗ₜ[R] ↑x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.compNatIsoDiscrete_inv_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D)
  (X : CategoryTheory.Discrete I),
  (CategoryTheory.Discrete.compNatIsoDiscrete F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α} {fallback : Unit},
  Std.DHashMap.Const.getD (Std.DHashMap.Const.unitOfList l) k fallback = ()
-- Mathlib.Data.Fintype.EquivFin
Infinite.set : ∀ {α : Type u_1} [Infinite α], Infinite (Set α)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.mulEquiv.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Mul β], e.mulEquiv = { toEquiv := e, map_mul' := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.move.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ]
  (a : Turing.Dir) (a_1 : Turing.TM1.Stmt Γ Λ σ), sizeOf (Turing.TM1.Stmt.move a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- Note that `degreeOf_pow_eq` proves equality with `NoZeroDivisors R` and nonzero polynomials.
 -/
MvPolynomial.degreeOf_pow_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ) (p : MvPolynomial σ R) (n : ℕ),
  MvPolynomial.degreeOf i (p ^ n) ≤ n * MvPolynomial.degreeOf i p
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).leadingCoeff = a
-- Mathlib.Algebra.Lie.Basic
LieEquiv.coe_coe : ∀ {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₂] (e : L₁ ≃ₗ⁅R⁆ L₂), ⇑e.toLieHom = ⇑e
-- Mathlib.Data.ENat.Basic
instLEENat : LE ℕ∞
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_top : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (f : PrincipalSeg r s), (Ordinal.typein s).toRelEmbedding f.top = Ordinal.type r
-- Mathlib.Algebra.Group.Irreducible.Lemmas
addIrreducible_isAddUnit_add : ∀ {M : Type u_2} [inst : AddMonoid M] {x y : M}, IsAddUnit x → (AddIrreducible (x + y) ↔ AddIrreducible y)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_strictMonoOn : ∀ {α : Type u}, StrictMonoOn (Cardinal.mk ∘ Set.Elem) {s | s.Finite}
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_prod_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.fst.prod AddMonoid.Coprod.snd = AddMonoid.Coprod.toProd
-- Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
/-- Given two cokernel coforks `c₁` and `c₂` for `f₁ : X₁ ⟶ Y₁` and `f₂ : X₂ ⟶ Y₂`,
this is the cokernel cofork for `(X₁ ⊗ Y₂) ⨿ (Y₁ ⊗ X₂) ⟶ Y₁ ⊗ Y₂` with
point `c₁.pt ⊗ c₂.pt`.  -/
CategoryTheory.Limits.CokernelCofork.tensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.MonoidalPreadditive C] →
          {X₁ Y₁ : C} →
            {f₁ : X₁ ⟶ Y₁} →
              CategoryTheory.Limits.CokernelCofork f₁ →
                {X₂ Y₂ : C} →
                  {f₂ : X₂ ⟶ Y₂} →
                    CategoryTheory.Limits.CokernelCofork f₂ →
                      [inst_4 :
                          CategoryTheory.Limits.HasBinaryCoproduct
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂)
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] →
                        CategoryTheory.Limits.CokernelCofork
                          (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Y₂)
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ f₂))
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.toLinearEquiv_quotientEquivOfIsTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  ↑(p.quotientEquivOfIsTopCompl q h) = p.quotientEquivOfIsCompl q ⋯
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.mk : ∀ {L : Type u_2} [inst : LieRing L] {h e f : L},
  h ≠ 0 → ⁅e, f⁆ = h → ⁅h, e⁆ = 2 • e → ⁅h, f⁆ = -(2 • f) → IsSl2Triple h e f
-- Init.Data.BitVec.Lemmas
BitVec.intMin_eq_zero_iff : ∀ {w : ℕ}, BitVec.intMin w = 0#w ↔ w = 0
-- Batteries.Data.List.Basic
/-- `List.mapWithComplement f l` is a variant of `List.mapWithPrefixSuffix`
that maps `f` across a list `l`.
For each `a ∈ l` with `l = pref ++ [a] ++ suff`, `a` is mapped to `f a (pref ++ suff)`,
i.e., the list input to `f` is `l` with `a` removed.
Example: if `f : Nat → list Nat → β`, `List.mapWithComplement f [1, 2, 3]` will produce the list
`[f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]]`.
 -/
List.mapWithComplement : {α : Type u_1} → {β : Type u_2} → (α → List α → β) → List α → List β
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.mul_comp_neg_X : ∀ {R : Type u_1} [inst : Ring R] (p q : Polynomial R),
  (p * q).comp (-Polynomial.X) = p.comp (-Polynomial.X) * q.comp (-Polynomial.X)
-- Mathlib.Data.TwoPointing
TwoPointing.toProd : {α : Type u_3} → TwoPointing α → α × α
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsProperSemilinearSet.isSemilinearSet : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s : Set M}, IsProperSemilinearSet s → IsSemilinearSet s
-- Init.Data.List.Nat.Erase
List.getElem_eraseIdx_of_lt : ∀ {α : Type u_1} {l : List α} {i j : ℕ} (h : j < (l.eraseIdx i).length), j < i → (l.eraseIdx i)[j] = l[j]
-- Mathlib.RingTheory.SimpleModule.Basic
isSemisimpleModule_iff : ∀ (R : Type u_2) [inst : Ring R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSemisimpleModule R M ↔ ComplementedLattice (Submodule R M)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_ball_inv_nat_pos : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.ball x (1 / ↑n)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.EditableDocumentCore.mk.injEq : ∀ («meta» : Lean.Server.DocumentMeta) (initSnap : Lean.Language.Lean.InitialSnapshot)
  (cmdSnaps : Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot)
  (diagnosticsMutex : Std.Mutex Lean.Server.FileWorker.DiagnosticsState) (meta_1 : Lean.Server.DocumentMeta)
  (initSnap_1 : Lean.Language.Lean.InitialSnapshot)
  (cmdSnaps_1 : Lean.AsyncList IO.Error Lean.Server.Snapshots.Snapshot)
  (diagnosticsMutex_1 : Std.Mutex Lean.Server.FileWorker.DiagnosticsState),
  ({ «meta» := «meta», initSnap := initSnap, cmdSnaps := cmdSnaps, diagnosticsMutex := diagnosticsMutex } =
      { «meta» := meta_1, initSnap := initSnap_1, cmdSnaps := cmdSnaps_1, diagnosticsMutex := diagnosticsMutex_1 }) =
    («meta» = meta_1 ∧ initSnap = initSnap_1 ∧ cmdSnaps = cmdSnaps_1 ∧ diagnosticsMutex = diagnosticsMutex_1)
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of an element of `K`.  -/
Height.logHeight₁ : {K : Type u_1} → [inst : Field K] → [Height.AdmissibleAbsValues K] → K → ℝ