mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableAux.mk.inj : ∀ {Γ₀ Γ₁ : Type} {tm : Turing.FinTM2} {inputAlphabet : tm.Γ tm.k₀ ≃ Γ₀} {outputAlphabet : tm.Γ tm.k₁ ≃ Γ₁}
  {tm_1 : Turing.FinTM2} {inputAlphabet_1 : tm_1.Γ tm_1.k₀ ≃ Γ₀} {outputAlphabet_1 : tm_1.Γ tm_1.k₁ ≃ Γ₁},
  { tm := tm, inputAlphabet := inputAlphabet, outputAlphabet := outputAlphabet } =
      { tm := tm_1, inputAlphabet := inputAlphabet_1, outputAlphabet := outputAlphabet_1 } →
    tm = tm_1 ∧ inputAlphabet ≍ inputAlphabet_1 ∧ outputAlphabet ≍ outputAlphabet_1
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {inst : CommSemiring R} {inst_1 : Semiring A}
  {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : DecidableEq ι} {inst_6 : AddMonoid ι}
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {inst_7 : GradedAlgebra 𝒜} {inst_8 : GradedAlgebra ℬ}
  {toAlgHom : A →ₐ[R] B} {map_mem : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom.toRingHom x ∈ ℬ i} {toAlgHom_1 : A →ₐ[R] B}
  {map_mem_1 : ∀ {i : ι} {x : A}, x ∈ 𝒜 i → toAlgHom_1.toRingHom x ∈ ℬ i},
  { toAlgHom := toAlgHom, map_mem := map_mem } = { toAlgHom := toAlgHom_1, map_mem := map_mem_1 } →
    toAlgHom = toAlgHom_1
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
TensorPower.toTensorAlgebra_gOne : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorPower.toTensorAlgebra GradedMonoid.GOne.one = 1
-- Lean.Elab.MutualDef
/-- Convert terms of the form `OfNat <type> (OfNat.ofNat Nat <num> ..)` into `OfNat <type> <num>`.
We use this method on instance declaration types.
The motivation is to address a recurrent mistake when users forget to use `nat_lit` when declaring `OfNat` instances.
See issues #1389 and #875
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.cleanupOfNat : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.linearization_map : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] {X Y : Action (Type w) G} (f : X ⟶ Y),
  (Rep.linearization k G).map f = Rep.ofHom (Representation.linearizeMap f)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringLeft_obj_map : ∀ (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] (F : C ⥤ₑ D) {X Y : D ⥤ₑ E} (f : X ⟶ Y),
  ((CategoryTheory.ExactFunctor.whiskeringLeft C D E).obj F).map f =
    CategoryTheory.ObjectProperty.homMk (F.obj.whiskerLeft f.hom)
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.nsmul_right_strictMonoOn : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {X : Finset G},
  0 ∈ X → X.Nontrivial → StrictMonoOn (fun n => n • X) {n | (n - 1) • ↑X ≠ ↑(AddSubgroup.closure ↑X)}
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_comp_iff_forall : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m (Matrix n n α)},
  ((Matrix.comp m m n n α) A).IsSymm ↔ ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- **Alias** of the reverse direction of `Set.one_notMem_div_iff`. -/
Disjoint.one_notMem_div_set : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, Disjoint s t → 1 ∉ s / t
-- Mathlib.Data.Nat.Prime.Defs
/-- The type of prime numbers  -/
Nat.Primes : Type
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.bijective_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.IsIso f], Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_sSup_of_mem : ∀ {M : Type u_2} [inst : Mul M] {S : Set (Subsemigroup M)} {s : Subsemigroup M}, s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
-- Mathlib.RingTheory.Ideal.Maps
Ideal.coheight_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Ring R] [inst_1 : Ring S] [inst_2 : FunLike F R S]
  [inst_3 : RingHomClass F R S] (f : F),
  Function.Surjective ⇑f → ∀ (I : Ideal S), Order.coheight (Ideal.comap f I) = Order.coheight I
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber → f = g
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_mk' : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ P₂) (e' : V₁ ≃ₗ[k] V₂) (p : P₁)
  (h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p), (AffineEquiv.mk' (⇑e) e' p h).linear = e'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ))
  (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv
      (CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)).mor₃ =
    -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_singleton : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : DecidableLE α] [inst_2 : OrderTop α] (b a : α),
  {b}.truncatedSup a = if a ≤ b then b else ⊤
-- Init.Grind.Lemmas
Lean.Grind.getElem_congr : ∀ {coll : Type u} {idx : Type v} {elem : Type w} {valid : coll → idx → Prop} [inst : GetElem coll idx elem valid]
  {as bs : coll} {i j : idx} {w₁ : valid as i} {a : elem},
  as = bs → i = j → (∀ (w₂ : valid bs j), bs[j] = a) → as[i] = a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nhds_basis_closedBall_pow : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r : ℝ},
  0 < r → r < 1 → (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (r ^ n)
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} [inst_7 : SizeOf 𝕜] [inst_8 : SizeOf E] [inst_9 : SizeOf F]
  (decDom : FredholmDecomposition 𝕜 E) (decCodom : FredholmDecomposition 𝕜 F) (equiv : ↥decDom.X₁ ≃L[𝕜] ↥decCodom.X₁)
  (eq_equiv : u = decCodom.X₁.subtypeL ∘SL ↑equiv ∘SL decDom.proj),
  sizeOf { decDom := decDom, decCodom := decCodom, equiv := equiv, eq_equiv := eq_equiv } =
    1 + sizeOf decDom + sizeOf decCodom + sizeOf equiv + sizeOf eq_equiv
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.restrict_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p), (f.restrict hf) x = ⟨f ↑x, ⋯⟩
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).obj₁ = X
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
/-- The natural isomorphism `(Γ₀.splitting K).nondegComplex ≅ K` for `K : ChainComplex C ℕ`.  -/
AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        AlgebraicTopology.DoldKan.Γ₀'.comp CategoryTheory.SimplicialObject.Split.nondegComplexFunctor ≅
          CategoryTheory.Functor.id (ChainComplex C ℕ)
-- Mathlib.Data.Finset.Sort
Finset.orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb : ∀ {n : ℕ} (i : Fin (n + 1)), {i}ᶜ.orderEmbOfFin ⋯ = i.succAboveOrderEmb
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.postcomp_injective : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : Zero X] [inst_1 : Zero Y] [inst_2 : Zero R]
  [inst_3 : TopologicalSpace X] [inst_4 : TopologicalSpace Y] [inst_5 : TopologicalSpace R] (g : ContinuousMapZero Y R),
  Function.Injective ⇑g → Function.Injective g.comp
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.get' : Lean.Meta.Grind.GoalM Lean.Meta.Grind.AC.State
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- If `F` is cover-preserving and compatible-preserving, then `F` is a continuous functor.  -/
CategoryTheory.Functor.isContinuous_of_coverPreserving : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D},
  CategoryTheory.CompatiblePreserving K F → CategoryTheory.CoverPreserving J K F → F.IsContinuous J K
-- Init.Data.List.Sublist
List.infix_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₁ ++ l₂
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.instantiateValueLevelParams : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure →
  List Lean.Name → List Lean.Level → Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.IsEquivalence.full : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.IsEquivalence], F.Full
-- Std.Data.DHashMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.DHashMap.insertIfNew : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → (a : α) → β a → Std.DHashMap α β
-- Mathlib.Topology.Closure
interior_subset_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s ⊆ closure s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Differentiable.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ},
  Differentiable ℂ f → Differentiable ℂ fun x => Complex.sin (f x)
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D`, `Y : GradedObject J D` and
`p : I × J → J` such that `p ⟨0, j⟩ = j` for all `j`,
this is the left unitor isomorphism `mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y`.  -/
CategoryTheory.GradedObject.mapBifunctorLeftUnitor : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
                    (X : C) →
                      (F.obj X ≅ CategoryTheory.Functor.id D) →
                        [∀ (Y : D),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] →
                          (p : I × J → J) →
                            (∀ (j : J), p (0, j) = j) →
                              (Y : CategoryTheory.GradedObject J D) →
                                [inst_6 :
                                    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj
                                              ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
                                          Y).HasMap
                                      p] →
                                  CategoryTheory.GradedObject.mapBifunctorMapObj F p
                                      ((CategoryTheory.GradedObject.single₀ I).obj X) Y ≅
                                    Y
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If `C` is finite as a CW complex then the collection of all cells (of any dimension) is
finite.  -/
Topology.RelCWComplex.finite_cells_of_finite : ∀ {X : Type u_2} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [finite : Topology.RelCWComplex.Finite C], Finite ((n : ℕ) × Topology.RelCWComplex.cell C n)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- Although `fun x => x ^ r` for fixed `r` is *not* complex-differentiable along the negative real
line, it is still real-differentiable, and the derivative is what one would formally expect.
See `hasDerivAt_ofReal_cpow_const` for an alternate formulation.  -/
hasDerivAt_ofReal_cpow_const' : ∀ {x : ℝ}, x ≠ 0 → ∀ {r : ℂ}, r ≠ -1 → HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
-- Mathlib.Algebra.Order.Monoid.Units
Units.instLinearOrder : {α : Type u_1} → [inst : Monoid α] → [LinearOrder α] → LinearOrder αˣ
-- Mathlib.Topology.Subpath
/-- Given two sequences of paths `F` and `G`, and a sequence `H` of homotopies between them,
there is a natural homotopy between `concat _ F` and `concat _ G`.  -/
Path.Homotopy.concat : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {n : ℕ} →
      (p : Fin (n + 1) → X) →
        (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
          ((k : Fin n) → (F k).Homotopy (G k)) → (Path.concat p F).Homotopy (Path.concat p G)
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.copy_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : CocompactMap α β)
  (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.GroupWithZero.Action.Pi
/-- A version of `Pi.single_smul` for non-dependent functions. It is useful in cases where Lean
fails to apply `Pi.single_smul`.  -/
Pi.single_smul' : ∀ {I : Type u} {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : DistribMulAction α β]
  [inst_3 : DecidableEq I] (i : I) (r : α) (x : β), Pi.single i (r • x) = r • Pi.single i x
-- Mathlib.Algebra.Group.Subgroup.Even
Submonoid.mem_square : ∀ {M : Type u_1} [inst : CommMonoid M] {a : M}, a ∈ Submonoid.square M ↔ IsSquare a
-- Mathlib.Order.SuccPred.CompleteLinearOrder
Order.IsSuccPrelimit.iSup_Iio : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, Order.IsSuccPrelimit x → ⨆ a, ↑a = x
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.main : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Integral.IntervalAverage
interval_average_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ),
  ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
-- Mathlib.GroupTheory.DivisibleHull
/-- If `f : M → ℕ+ → α` respects the equivalence on localization,
lift it to a function `DivisibleHull M → α`.  -/
DivisibleHull.liftOn : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {α : Type u_2} →
      DivisibleHull M →
        (f : M → ℕ+ → α) →
          (∀ (m m' : M) (s s' : ℕ+), DivisibleHull.mk m s = DivisibleHull.mk m' s' → f m s = f m' s') → α
-- Init.Data.Float.Float
/-- Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller
than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`ceil`.

Examples:
 * `Float.ceil 1.5 = 2`
 * `Float.ceil (-1.5) = (-1)`
 -/
Float.ceil : Float → Float
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- **Alias** of the reverse direction of `Real.sinh_ne_zero`. -/
Mathlib.Meta.Positivity.sinh_ne_zero_of_ne_zero : ∀ {x : ℝ}, x ≠ 0 → Real.sinh x ≠ 0
-- Batteries.Control.ForInStep.Basic
/-- Get the value out of a `ForInStep`.
This is usually done at the end of a `forIn` loop to scope the early exit to the loop body.
 -/
ForInStep.run : {α : Type u_1} → ForInStep α → α
-- Mathlib.Analysis.Real.Hyperreal
/-- A hyperreal number is negative infinite if it is smaller than all real numbers.
**Do not use.** Write `x < 0 ∧ ArchimedeanClass.mk x < 0` instead.  -/
Hyperreal.InfiniteNeg : ℝ* → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_eq_head_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he = t.keys.head ⋯
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_uInt64ToNat : ∀ (n : UInt64) (h : n.toNat < UInt16.size), UInt16.ofNatLT n.toNat h = n.toUInt16
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.inv_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {X Y : CategoryTheory.Comma L R} (e : Y ⟶ X) [inst_3 : CategoryTheory.IsIso e],
  (CategoryTheory.inv e).right = CategoryTheory.inv e.right
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `ringChar F` is odd, then `quadraticChar F a` can be computed in
terms of `a ^ (Fintype.card F / 2)`.  -/
quadraticChar_eq_pow_of_char_ne_two : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∀ {a : F}, a ≠ 0 → (quadraticChar F) a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1
-- Mathlib.Algebra.Algebra.ZMod
/-- The `ZMod n`-algebra structure on rings whose characteristic `m` divides `n`.
See note [reducible non-instances].  -/
ZMod.algebra' : (R : Type u_1) → [inst : Ring R] → {n : ℕ} → (m : ℕ) → [CharP R m] → m ∣ n → Algebra (ZMod n) R
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.unop_f' : ∀ {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), h.unop.f' = h.g'.unop
-- Mathlib.Topology.MetricSpace.Algebra
MulOpposite.lipschitzMul : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [LipschitzMul β], LipschitzMul βᵐᵒᵖ
-- Init.Data.List.Basic
/-- Returns the slice of `l` from indices `start` (inclusive) to `stop` (exclusive).

Examples:
* [0, 1, 2, 3, 4, 5].extract 1 2 = [1]
* [0, 1, 2, 3, 4, 5].extract 2 2 = []
* [0, 1, 2, 3, 4, 5].extract 2 4 = [2, 3]
* [0, 1, 2, 3, 4, 5].extract 2 = [2, 3, 4, 5]
* [0, 1, 2, 3, 4, 5].extract (stop := 2) = [0, 1]
 -/
List.extract : {α : Type u} → (l : List α) → optParam ℕ 0 → optParam ℕ l.length → List α
-- Std.Data.DTreeMap.Raw.Basic
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Raw.Equiv.inner : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id a)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom h =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f)) h))
-- Mathlib.Data.List.ReduceOption
List.reduceOption_length_eq_iff : ∀ {α : Type u_1} {l : List (Option α)}, l.reduceOption.length = l.length ↔ ∀ x ∈ l, x.isSome = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_alter_of_compare_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      cmp k k' = Ordering.eq →
        (k' ∈ Std.DTreeMap.Raw.Const.alter t k f ↔ (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true)
-- Lean.Parser.Extension
Lean.Parser.categoryParserFnImpl : Lean.Name → Lean.Parser.ParserFn
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The canonical projection from the `I`-adic completion to `R ⧸ I`.  -/
AdicCompletion.evalOneₐ : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → AdicCompletion I R →ₐ[R] R ⧸ I
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) [w.GuitartExact]
  (F : CategoryTheory.Functor C₂ D) [R.HasPointwiseLeftKanExtension F], L.HasPointwiseLeftKanExtension (T.comp F)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {ea eb : Lean.Grind.AC.Expr} {a_1 b_1 : Lean.Expr} {ea_1 eb_1 : Lean.Grind.AC.Expr},
  Lean.Meta.Grind.AC.EqCnstrProof.core a b ea eb = Lean.Meta.Grind.AC.EqCnstrProof.core a_1 b_1 ea_1 eb_1 →
    a = a_1 ∧ b = b_1 ∧ ea = ea_1 ∧ eb = eb_1
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colon_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom).app X)
      (CategoryTheory.CategoryStruct.comp ((Φ.colon Ψ).ι.app X) h) =
    CategoryTheory.CategoryStruct.comp (Φ.ι.app X) h
-- Mathlib.Order.CompleteLattice.Defs
iInf_lt_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {a : α} {f : ι → α}, iInf f < a ↔ ∃ i, f i < a
-- Lean.Elab.Parallel
/-- Runs a list of CoreM computations in parallel and returns:
* a combined cancellation hook for all tasks, and
* an iterator that yields results in original order.

The iterator runs in CoreM, and as it yields each result, it updates the CoreM state
to reflect the state when that particular task completed. This means the state is
threaded through the iteration in the order of the original list.

Results are wrapped in `Except Exception α` so that errors in individual tasks don't stop
the iteration - you can observe all results including which tasks failed.

The iterator will terminate after all jobs complete (assuming they all do complete).
 -/
Lean.Core.CoreM.parIterWithCancel : {α : Type} → List (Lean.CoreM α) → Lean.CoreM (BaseIO PUnit.{1} × Std.IterM Lean.CoreM (Except Lean.Exception α))