mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_yield_eq_foldM : ∀ {α β : Type w} {γ δ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ} {it : Std.Iter β},
  (forIn it init fun c b => (fun d => ForInStep.yield (g c b d)) <$> f c b) =
    Std.Iter.foldM (fun b c => g c b <$> f c b) init it
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_image_nhds_mem_nhds_of_boundaryless : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] [I.Boundaryless] {x : M},
  s ∈ nhds x → ↑(extChartAt I x) '' s ∈ nhds (↑(extChartAt I x) x)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_mod_two_eq_one : ∀ {x i : ℕ}, x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R], m.degree 1 = 0
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L]
  (I : LieIdeal R L), LieModule.IsNilpotent L ↥I ↔ I ≤ LieAlgebra.maxNilpotentIdeal R L
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_inv_comp_iCycles : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv (groupHomology.iCycles A 0) =
    (groupHomology.chainsIso₀ A).inv
-- Lean.Elab.Term.TermElabM
/-- Auxiliary method for reporting errors of the form "... contains metavariables ...".
This kind of error is thrown, for example, at `Match.lean` where elaboration
cannot continue if there are metavariables in patterns.
We only want to log it if we haven't logged any errors so far.  -/
Lean.Elab.Term.throwMVarError : {α : Type} → Lean.MessageData → Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) h) =
    h
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_centralizer_iff : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A} {z : A},
  z ∈ Subalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g
-- Init.Data.Vector.Lemmas
Vector.toList_append : ∀ {α : Type u_1} {m n : ℕ} {xs : Vector α m} {ys : Vector α n}, (xs ++ ys).toList = xs.toList ++ ys.toList
-- Mathlib.Order.TypeTags
WithBot.bot : {α : Type u_1} → Bot (WithBot α)
-- Mathlib.Topology.UniformSpace.Basic
IsClosed.relPreimage_of_finite : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → ∀ {t : Set β}, t.Finite → IsClosed (s.preimage t)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.get! a = t.getD a default
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.measurePreserving_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure ν],
  MeasureTheory.MeasurePreserving Prod.fst (μ.prod ν) μ
-- Std.Data.TreeMap.Basic
/-- Returns the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeMap.keyAtIdxD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → ℕ → α → α
-- Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
CategoryTheory.ParametrizedAdjunction.preservesLimitsOfShape_flip_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) (J : Type u_4)
  [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  [∀ (X₂ : C₂), CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ (F.flip.obj X₂)] (X₃ : C₃),
  CategoryTheory.Limits.PreservesLimitsOfShape J (G.flip.obj X₃)
-- Mathlib.Order.Filter.Finite
Set.PairwiseDisjoint.exists_mem_filter : ∀ {α : Type u} {ι : Type u_2} {l : ι → Filter α} {t : Set ι},
  t.PairwiseDisjoint l → t.Finite → ∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
-- Init.System.IO
IO.FS.Stream.Buffer.mk.injEq : ∀ (data : ByteArray) (pos : ℕ) (data_1 : ByteArray) (pos_1 : ℕ),
  ({ data := data, pos := pos } = { data := data_1, pos := pos_1 }) = (data = data_1 ∧ pos = pos_1)
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivAt.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} [inst_7 : Fintype ι],
  HasFDerivAt c c' x → ∀ (u : (i : ι) → M i), HasFDerivAt (fun y => (c y) u) (c'.flipMultilinear u) x
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Push forward a `MulZeroClass` instance along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.mulZeroClass : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : MulZeroClass M₀] →
      [inst_1 : Mul M₀'] →
        [inst_2 : Zero M₀'] →
          (f : M₀ → M₀') → Function.Surjective f → f 0 = 0 → (∀ (a b : M₀), f (a * b) = f a * f b) → MulZeroClass M₀'
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_3 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (Std.ExtTreeMap.ofList l cmp)[k]! = default
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_le_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalRing R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f g : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_le_iff._auto_1 →
    autoParam (ContinuousOn g (quasispectrum R a)) cfcₙ_le_iff._auto_3 →
      autoParam (f 0 = 0) cfcₙ_le_iff._auto_5 →
        autoParam (g 0 = 0) cfcₙ_le_iff._auto_7 →
          autoParam (p a) cfcₙ_le_iff._auto_9 → (cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ quasispectrum R a, f x ≤ g x)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (V : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).inverse.obj V).str =
    (adj.homEquiv V.V V.V).symm V.str
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_31 : HSub Std.Time.Day.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.filter_apply : ∀ {α : Type u_1} {p : PMF α} {s : Set α} (h : ∃ a ∈ s, a ∈ p.support) (a : α),
  (p.filter s h) a = s.indicator (⇑p) a * (∑' (a' : α), s.indicator (⇑p) a')⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full]
  [F.Faithful], CategoryTheory.CategoryStruct.comp (hf.lift i h hi) (hf.snd g) = h
-- Mathlib.Data.List.Pi
/-- Given `α : ι → Sort*`, `Pi.nil α` is the trivial dependent function out of the empty list.  -/
List.Pi.nil : {ι : Type u_1} → (α : ι → Sort u_3) → (i : ι) → i ∈ [] → α i
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.mk.inj : ∀ {applyEdit? : Option Bool} {workspaceEdit? : Option Lean.Lsp.WorkspaceEditClientCapabilities}
  {applyEdit?_1 : Option Bool} {workspaceEdit?_1 : Option Lean.Lsp.WorkspaceEditClientCapabilities},
  { applyEdit? := applyEdit?, workspaceEdit? := workspaceEdit? } =
      { applyEdit? := applyEdit?_1, workspaceEdit? := workspaceEdit?_1 } →
    applyEdit? = applyEdit?_1 ∧ workspaceEdit? = workspaceEdit?_1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- Given `obj : Fin (n + 1) → C` and `mapSucc i : obj i.castSucc ⟶ obj i.succ`
for all `i : Fin n`, this is `F : ComposableArrows C n` such that `F.obj i` is
definitionally equal to `obj i` and such that `F.map' i (i + 1) = mapSucc ⟨i, hi⟩`.  -/
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      (obj : Fin (n + 1) → C) → ((i : Fin n) → obj i.castSucc ⟶ obj i.succ) → CategoryTheory.ComposableArrows C n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorem.mk.injEq : ∀ (funPropName thmName : Lean.Name) (thmArgs : Mathlib.Meta.FunProp.LambdaTheoremArgs)
  (funPropName_1 thmName_1 : Lean.Name) (thmArgs_1 : Mathlib.Meta.FunProp.LambdaTheoremArgs),
  ({ funPropName := funPropName, thmName := thmName, thmArgs := thmArgs } =
      { funPropName := funPropName_1, thmName := thmName_1, thmArgs := thmArgs_1 }) =
    (funPropName = funPropName_1 ∧ thmName = thmName_1 ∧ thmArgs = thmArgs_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h : k' ∈ Std.ExtDHashMap.Const.unitOfList l}, (Std.ExtDHashMap.Const.unitOfList l).getKey k' h = k
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk'_eq_mk' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (x : M), Quotient.mk' x = Submodule.Quotient.mk x
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_eq_matrix_trace : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (b : Module.Basis ι R M) (f : M →ₗ[R] M),
  (LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram `D` to `F` is limit
of `F` evaluated at `D`. This variant is for contravariant diagrams, see
`colimitCoyonedaHomIsoLimit'` for a covariant version.  -/
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor Iᵒᵖ C) →
          (F : CategoryTheory.Functor C (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.rightOp.comp CategoryTheory.coyoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.IndParallelPairPresentation.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} →
        (I : Type v₁) →
          [ℐ : CategoryTheory.SmallCategory I] →
            [hI : CategoryTheory.IsFiltered I] →
              (F₁ F₂ : CategoryTheory.Functor I C) →
                (ι₁ : F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A) →
                  (isColimit₁ : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁ }) →
                    (ι₂ : F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj B) →
                      CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂ } →
                        (φ ψ : F₁ ⟶ F₂) →
                          f =
                              isColimit₁.map { pt := B, ι := ι₂ }
                                (CategoryTheory.Functor.whiskerRight φ CategoryTheory.yoneda) →
                            g =
                                isColimit₁.map { pt := B, ι := ι₂ }
                                  (CategoryTheory.Functor.whiskerRight ψ CategoryTheory.yoneda) →
                              CategoryTheory.IndParallelPairPresentation f g
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.eq_neg_one_iff' : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℕ}, legendreSym p ↑a = -1 ↔ ¬IsSquare ↑a
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The Grothendieck group of a monoid `M` is the localization at its top submonoid.  -/
Algebra.GrothendieckGroup : (M : Type u_1) → [CommMonoid M] → Type u_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.bypass.eq_def : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} (x : G.Walk u v),
  x.bypass =
    match v, x with
    | .(u), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil
    | v, SimpleGraph.Walk.cons ha p =>
      have p' := p.bypass;
      if hs : u ∈ p'.support then p'.dropUntil u hs else SimpleGraph.Walk.cons ha p'
-- Lean.Level
Lean.instBEqData : BEq Lean.Level.Data
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfMkEqMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f f_1 : A₁ ⟶ B) (e_f : f = f_1)
  (g g_1 : A₂ ⟶ B) (e_g : g = g_1) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g),
  CategoryTheory.Subobject.isoOfMkEqMk f g h = CategoryTheory.Subobject.isoOfMkEqMk f_1 g_1 ⋯
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_uInt32ToNat : ∀ (n : UInt32), UInt64.ofNatClamp n.toNat = n.toUInt64
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.topCatAdjunctionCounit_bijective : ∀ (X : TopCat), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (CondensedSet.topCatAdjunctionCounit X))
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_eq_zero_iff : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] (x : ℕ), ↑x = 0 ↔ x % p = 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then
in a neighborhood of `x`, the term of order `1` of this series is a derivative of `f`.  -/
HasFTaylorSeriesUpToOn.eventually_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s →
    n ≠ 0 → s ∈ nhds x → ∀ᶠ (y : E) in nhds x, HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p y 1)) y
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.coe_subtype : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M),
  ⇑S.subtype = Subtype.val
-- Mathlib.Algebra.Group.Irreducible.Lemmas
IsSquare.not_irreducible : ∀ {M : Type u_2} [inst : Monoid M] {x : M}, IsSquare x → ¬Irreducible x
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_zero : ∀ {X : Type u_1} [inst : MeasurableSpace X] (x y : X),
  ProbabilityTheory.bernoulliMeasure x y 0 = MeasureTheory.Measure.dirac y
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWithMAux.eq_1 : ∀ {α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (bs : Array β)
  (f : α → β → m γ) (i : ℕ) (cs : Array γ),
  as.zipWithMAux bs f i cs =
    if h : i < as.size then
      have a := as[i];
      if h : i < bs.size then
        have b := bs[i];
        do
        let __do_lift ← f a b
        as.zipWithMAux bs f (i + 1) (cs.push __do_lift)
      else pure cs
    else pure cs
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) {Z_1 : D}
  (h : L.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f₁ g)
        (CategoryTheory.CategoryStruct.comp f₂ g))
      h
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- Let `M'` be a manifold whose chart structure is given by an open embedding `e'` into its model
space `H'`. If `e' ∘ f : M → H'` is `C^n`, then `f` is `C^n`.

This is useful, for example, when `e' ∘ f = g ∘ e` for smooth maps `e : M → X` and `g : X → H'`.  -/
ContMDiff.of_comp_isOpenEmbedding : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {n : WithTop ℕ∞} [inst_9 : ChartedSpace H M] [inst_10 : Nonempty M'] {e' : M' → H'}
  (h' : Topology.IsOpenEmbedding e') {f : M → M'}, ContMDiff I I' n (e' ∘ f) → ContMDiff I I' n f
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.mem_centralizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {s : Set G}, g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, h + g = g + h
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.id : {α : Type} → Std.Bounded.Receiver✝ α → ℕ
-- Lean.Parser.Term.Basic
Lean.Parser.Term.typeSpec : Lean.Parser.Parser
-- Mathlib.Algebra.RingQuot
/-- If two `S`-algebras are `S`-equivalent and their quotients by a relation `rel` are defined,
then their quotients are also `S`-equivalent.

(Special case of the third isomorphism theorem.)  -/
RingQuot.algEquivQuotAlgEquiv : {S : Type uS} →
  [inst : CommSemiring S] →
    {A : Type uA} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra S A] →
          {B : Type u₄} →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra S B] →
                (f : A ≃ₐ[S] B) → (rel : A → A → Prop) → RingQuot rel ≃ₐ[S] RingQuot (Function.onFun rel ⇑f.symm)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.prodMk_space : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {E'' : Type u_8} [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E'']
  {s : Set M} {f : M → E'} {g : M → E''}, MDiff[s] f → MDiff[s] g → MDiff[s] fun x => (f x, g x)
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The proximity function `f * g` at `0` is less than or equal to the sum of the proximity functions of
`f` and `g`, respectively.
 -/
ValueDistribution.proximity_mul_zero_le : ∀ {f₁ f₂ : ℂ → ℂ},
  Meromorphic f₁ →
    Meromorphic f₂ →
      ValueDistribution.proximity (f₁ * f₂) 0 ≤ ValueDistribution.proximity f₁ 0 + ValueDistribution.proximity f₂ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The image of an edge by a morphism of simplicial sets.  -/
SSet.Edge.map : {X Y : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    SSet.Edge x₀ x₁ →
      (f : X ⟶ Y) →
        SSet.Edge ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₀)
          ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := 0 }))) x₁)