mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mono : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {i j : ι}
  (f : MeasureTheory.Filtration ι m), i ≤ j → ↑f i ≤ ↑f j
-- Mathlib.Data.FinEnum
FinEnum.instUInt64 : FinEnum UInt64
-- Mathlib.RingTheory.Flat.Basic
/-- If `M` is flat then `- ⊗ M` is an exact functor.  -/
Module.Flat.rTensor_exact : ∀ {R : Type u} (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  ⦃N : Type u_1⦄ ⦃N' : Type u_2⦄ ⦃N'' : Type u_3⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N']
  [inst_6 : AddCommGroup N''] [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄
  ⦃g : N' →ₗ[R] N''⦄, Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g)
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_left_iff : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {F : Type u_6}
  [inst_3 : FunLike F P₁ P₃] [DilationClass F P₁ P₃] (f : F), Similar (⇑f ∘ v₁) v₂ ↔ Similar v₁ v₂
-- Std.Data.DTreeMap.Raw.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.Raw.alter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] →
        Std.DTreeMap.Raw α β cmp → (a : α) → (Option (β a) → Option (β a)) → Std.DTreeMap.Raw α β cmp
-- Lean.Meta.Tactic.Generalize
/-- Telescopic `generalize` tactic. It can simultaneously generalize many terms.
It uses `kabstract` to occurrences of the terms that need to be generalized.
 -/
_private.Lean.Meta.Tactic.Generalize.0.Lean.Meta.generalizeCore : Lean.MVarId → Array Lean.Meta.GeneralizeArg → Lean.Meta.TransparencyMode → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Init.Prelude
/-- Replaces the value at (zero-based) index `n` in `l` with `a`. If the index is out of bounds, then
the list is returned unmodified.

Examples:
* `["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]`
* `["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]`
 -/
List.set : {α : Type u_1} → List α → ℕ → α → List α
-- Mathlib.Order.Max
IsMin.eq_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMin a → b ≤ a → a = b
-- Mathlib.Condensed.Explicit
/-- A `CondensedMod` version of `Condensed.ofSheafProfinite`.  -/
CondensedMod.ofSheafProfinite : (R : Type (u + 1)) →
  [inst : Ring R] →
    (F : CategoryTheory.Functor Profiniteᵒᵖ (ModuleCat R)) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → CondensedMod R
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableOn.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {s : Set E},
  DifferentiableOn 𝕜 f s → (∀ x ∈ s, f₁ x = f x) → DifferentiableOn 𝕜 f₁ s
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the sum of two vectors is less than or equal
to the sum of the `L_p`-seminorms of the summands. A version for `ℝ≥0∞`-valued nonnegative
functions.  -/
ENNReal.Lp_add_le : ∀ {ι : Type u} (s : Finset ι) (f g : ι → ENNReal) {p : ℝ},
  1 ≤ p → (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrixₛₗ₂'_symm : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m],
  (LinearMap.toMatrixₛₗ₂' R).symm = Matrix.toLinearMapₛₗ₂' R σ₁ σ₂
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.SameCycle.equivalence : ∀ {α : Type u_2} (f : Equiv.Perm α), Equivalence f.SameCycle
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {A B : CommHopfAlgCat R} {hom' hom'_1 : ↑A →ₐc[R] ↑B},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Order.Basic
lt_iff_le_and_ne' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b < a ↔ b ≤ a ∧ a ≠ b
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), WellFoundedLT (α i)], (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0) → WellFoundedLT (Π₀ (i : ι), α i)
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctorZero'_inv_app_f : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) (h : n = 0)
  (X : CochainComplex C ℤ) (i : ℤ),
  ((CochainComplex.shiftFunctorZero' C n h).inv.app X).f i = (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Lean.Widget.UserWidget
Lean.Widget.PanelWidgetInstance.mk.injEq : ∀ (toWidgetInstance : Lean.Widget.WidgetInstance) (range? : Option Lean.Lsp.Range) (name? : Option String)
  (toWidgetInstance_1 : Lean.Widget.WidgetInstance) (range?_1 : Option Lean.Lsp.Range) (name?_1 : Option String),
  ({ toWidgetInstance := toWidgetInstance, range? := range?, name? := name? } =
      { toWidgetInstance := toWidgetInstance_1, range? := range?_1, name? := name?_1 }) =
    (toWidgetInstance = toWidgetInstance_1 ∧ range? = range?_1 ∧ name? = name?_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.submonoidCongr.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S = T),
  MulEquiv.submonoidCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndHom.eq_1 : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (B : Rep.{u, u, u} k H),
  Rep.coinvariantsTensorIndHom φ A B =
    ModuleCat.ofHom
      (Representation.Coinvariants.lift
        (((CategoryTheory.MonoidalCategory.curriedTensor (Rep.{u, u, u} k H)).obj (Rep.ind φ A)).obj B).ρ
        (TensorProduct.lift
          (Representation.Coinvariants.lift
            (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
            (TensorProduct.lift
              (((Finsupp.lift
                    (↑A →ₗ[k]
                      ↑B →ₗ[k]
                        (((CategoryTheory.MonoidalCategory.curriedTensor (Rep.{u, u, u} k G)).obj A).obj
                              (Rep.res φ B)).ρ.Coinvariants)
                    k H)
                  fun g => (A.coinvariantsTensorMk (Rep.res φ B)).compl₂ (B.ρ g)) ∘ₗ
                ↑(MonoidAlgebra.coeffLinearEquiv k)))
            ⋯))
        ⋯)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.toOverIsoToOverUnit_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C),
  (CategoryTheory.toOverIsoToOverUnit.hom.app X).left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        ((CategoryTheory.equivToOverUnit C).unit.app
          ((CategoryTheory.toOver (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).obj X)))
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A linearly independent family is maximal if there is no strictly larger linearly independent family.
 -/
LinearIndependent.Maximal : {ι : Type w} →
  {R : Type u} →
    [inst : Semiring R] →
      {M : Type v} → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {v : ι → M} → LinearIndependent R v → Prop
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.mem_toGrothendieck : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Coverage C} {X : C}
  {S : CategoryTheory.Sieve X}, S ∈ K.toGrothendieck X ↔ K.Saturate X S
-- Mathlib.Order.Fin.Tuple
/-- Order isomorphism between tuples of length `n + 1` and pairs of an element and a tuple of length
`n` given by separating out the last element of the tuple.

This is `Fin.snoc` as an `OrderIso`.  -/
Fin.snocOrderIso : {n : ℕ} →
  (α : Fin (n + 1) → Type u_2) →
    [inst : (i : Fin (n + 1)) → LE (α i)] → α (Fin.last n) × ((i : Fin n) → α i.castSucc) ≃o ((i : Fin (n + 1)) → α i)
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given functors `F : C ⥤ D` and
`G : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ (Dᵒᵖ ⥤ Type max w v₁ v₂)`,
and a natural transformation `φ : F ⋙ uliftYoneda ⟶ uliftYoneda ⋙ G`, this is the
(natural) morphism `P ⟶ F.op ⋙ G.obj P` for all `P : Cᵒᵖ ⥤ Type max w v₁ v₂` that is
determined by `φ`.  -/
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G :
              CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
                (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))} →
            (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶
                CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G) →
              (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) → P ⟶ F.op.comp (G.obj P)
-- Mathlib.Tactic.Translate.Reorder
/-- Elaborate syntax that refers to an argument of a declaration or hypothesis.
This is either a 1-indexed number, or a name from `argNames`.
- `fvars` is only used to add hover information to `stx`
- `head` is only used for the error message.  -/
Mathlib.Tactic.Translate.elabArgStx : Lean.TSyntax [`ident, `num] → Array Lean.Name → Array Lean.Expr → Lean.MessageData → Lean.MetaM ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A), P.symm.I = P.I
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Transfer `AddMonObj` along an isomorphism.  -/
CategoryTheory.AddMonObj.ofIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M X : C} → [CategoryTheory.AddMonObj M] → (M ≅ X) → CategoryTheory.AddMonObj X
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.isStrictImplicit : Lean.Meta.ParamInfo → Bool
-- Init.Data.BitVec.Lemmas
BitVec.instCommutativeHOr : ∀ {w : ℕ}, Std.Commutative fun x y => x ||| y
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.commensurable_strictPeriods_periods : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)), 𝒢.strictPeriods.Commensurable 𝒢.periods
-- Mathlib.Data.FP.Basic
FP.emin.eq_1 : ∀ [C : FP.FloatCfg], FP.emin = 1 - ↑FP.FloatCfg.emax
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.iInter : ∀ {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [inst : LE α] [Nonempty ι] {f : ι → Set α},
  (∀ (i : ι), IsRelUpperSet (f i) P) → IsRelUpperSet (⋂ i, f i) P
-- Init.Data.List.Basic
List.Sublist.below : {α : Type u_1} → {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} → {a a_1 : List α} → a.Sublist a_1 → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.w_assoc : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] [inst_2 : SuccOrder ι] [inst_3 : NoMaxOrder ι] (j : ι) {Z : SSet}
  (h : (f.filtration (Order.succ j)).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.t j) (CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯) h) =
    CategoryTheory.CategoryStruct.comp (f.m j) (CategoryTheory.CategoryStruct.comp (f.b j) h)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extend_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X : C} (f : c.pt ⟶ X), (c.extend f).pt = X
-- Mathlib.Order.Hom.WithTopBot
Function.Embedding.coeWithTop_apply : ∀ {α : Type u_1} (a : α), Function.Embedding.coeWithTop a = ↑a
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoid.Coprod.swap M N).comp AddMonoid.Coprod.inr = AddMonoid.Coprod.inl
-- Mathlib.Topology.UniformSpace.Closeds
inv_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α), (hausdorffEntourage U).inv = hausdorffEntourage U.inv
-- Init.Data.Vector.Lemmas
Vector.getElem?_set!_ne : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α}, i ≠ j → (xs.set! i x)[j]? = xs[j]?
-- Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
/-- (implementation) Pulling out a colimit out of a hom functor is one half of the key lemma. Note
that all of the heavy lifting actually happens in `CostructuredArrow.toOverCompYonedaColimit`
and `yonedaYonedaColimit`.  -/
CategoryTheory.Limits.IndizationClosedUnderFilteredColimitsAux.compYonedaColimitIsoColimitCompYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type v} →
      [inst_1 : CategoryTheory.SmallCategory I] →
        (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) →
          {J : Type v} →
            [inst_2 : CategoryTheory.SmallCategory J] →
              (G :
                  CategoryTheory.Functor J
                    (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F))) →
                {K : Type v} →
                  [inst_3 : CategoryTheory.SmallCategory K] →
                    (H : CategoryTheory.Functor K (CategoryTheory.Over (CategoryTheory.Limits.colimit F))) →
                      (G.op.comp
                              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                  (CategoryTheory.Limits.colimit F)).op).comp
                          (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit H)) ≅
                        CategoryTheory.Limits.colimit
                          (H.comp
                            (CategoryTheory.yoneda.comp
                              ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ
                                    (CategoryTheory.Over (CategoryTheory.Limits.colimit F))ᵒᵖ (Type (max u v))).obj
                                (G.op.comp
                                  (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                      (CategoryTheory.Limits.colimit F)).op))))
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- **Alias** of `isClosed_setOfPred_isCompactOperator`.

---

The set of compact operators from a normed space to a complete topological vector space is
closed.  -/
isClosed_setOf_isCompactOperator : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : IsUniformAddGroup M₂]
  [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂], IsClosed {f | IsCompactOperator ⇑f}
-- Init.Data.Rat.Lemmas
Rat.inv_eq_of_mul_eq_one : ∀ {a b : ℚ}, a * b = 1 → a⁻¹ = b
-- Init.Prelude
Nat.lt_irrefl : ∀ (n : ℕ), ¬n < n
-- Init.Data.Fin.Lemmas
Fin.sub_eq_add_neg : ∀ {n : ℕ} (x y : Fin n), x - y = x + -y
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.neg : ∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] {φ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → (-φ).IsHomogeneous n
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Find a name in `ns` that starts with prefix `p`.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Lean.Name.prefixToName : Lean.Name → Array Lean.Name → Option Lean.Name
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_minValue : ∀ (h : System.Platform.numBits = 64), ISize.minValue.toBitVec64 h = BitVec.intMin 64
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalExprOccurrences : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Occurrences
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.not_isUniform_iff : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α},
  ¬G.IsUniform ε s t ↔
    ∃ s' ⊆ s, ∃ t' ⊆ t, ↑s.card * ε ≤ ↑s'.card ∧ ↑t.card * ε ≤ ↑t'.card ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|
-- Init.Data.Float.Float32
/-- Constructs a `Float32` from a `Float32.Model`.  -/
Float32.ofModel : Float32.Model → Float32
-- Std.Data.TreeMap.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.TreeMap.foldl : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → {δ : Type w} → (δ → α → β → δ) → δ → Std.TreeMap α β cmp → δ
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.unop_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : Cᵒᵖ} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  h.unop.i =
    CategoryTheory.Arrow.homMk (CategoryTheory.Arrow.Hom.right h.r).unop (CategoryTheory.Arrow.Hom.left h.r).unop ⋯
-- Lean.Meta.Tactic.Grind.Core
/-- Adds a new hypothesis.  -/
Lean.Meta.Grind.addHypothesis : Lean.FVarId → optParam ℕ 0 → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Nat.ModEq
Nat.mod_eq_of_modEq : ∀ {a b n : ℕ}, a ≡ b [MOD n] → b < n → a % n = b
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mem_def : ∀ {α : Type u_1} [inst : Preorder α] {s : NonemptyInterval α} {a : α}, a ∈ s ↔ s.toProd.1 ≤ a ∧ a ≤ s.toProd.2
-- Mathlib.Data.Nat.Prime.Defs
/-- If `n < k * k`, then `minFacAux n k = n`, if `k | n`, then `minFacAux n k = k`.
Otherwise, `minFacAux n k = minFacAux n (k+2)` using well-founded recursion.
If `n` is odd and `1 < n`, then `minFacAux n 3` is the smallest prime factor of `n`.

This definition is by well-founded recursion, so `rfl` or `decide` cannot be used.
One can use `norm_num` to prove `Nat.prime n` for small `n`.
 -/
Nat.minFacAux : ℕ → ℕ → ℕ
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- Algebra homomorphism mapping `w` to `fun v ↦ e (L v w)`.  -/
BoundedContinuousFunction.charAlgHom : {V : Type u_1} →
  {W : Type u_2} →
    [inst : AddCommGroup V] →
      [inst_1 : Module ℝ V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : AddCommGroup W] →
            [inst_4 : Module ℝ W] →
              [inst_5 : TopologicalSpace W] →
                {e : AddChar ℝ Circle} →
                  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} →
                    Continuous ⇑e →
                      (Continuous fun p => (L p.1) p.2) → AddMonoidAlgebra ℂ W →ₐ[ℂ] BoundedContinuousFunction V ℂ
-- Mathlib.Data.List.Sort
_private.Mathlib.Data.List.Sort.0.List.orderedInsert.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (b : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (b : α) → (l : List α) → motive (b :: l)),
  (match b :: l with
    | [] => h_1 ()
    | b :: l => h_2 b l) =
    h_2 b l
-- Mathlib.Order.Closure
ClosureOperator.closure_sup_closure_left : ∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c (c x ⊔ y) = c (x ⊔ y)
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Erase matches containing any of the hypotheses `hs` from `ms`.  -/
Aesop.ForwardRuleMatches.eraseHyps : Std.HashSet Lean.FVarId → Aesop.ForwardRuleMatches → Aesop.ForwardRuleMatches
-- Init.Data.List.Sublist
List.IsSuffix.isInfix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ <:+: l₂
-- Mathlib.Data.FP.Basic
FP.FloatCfg.mk : (prec emax : ℕ) → 0 < prec → prec ≤ emax → FP.FloatCfg
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Adjunction.fromCokleisli_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  {X x : CategoryTheory.Cokleisli U} (f : X ⟶ x),
  (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).map f =
    CategoryTheory.CategoryStruct.comp (U.δ.app X.of) (U.map f.of)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.uniq`. -/
CategoryTheory.Classifier.SubobjectRepresentableBy.uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω) {U X : C} {m : U ⟶ X} [inst_2 : CategoryTheory.Mono m] {χ' : X ⟶ Ω}
  {π : U ⟶ CategoryTheory.Subobject.underlying.obj h.Ω₀}, CategoryTheory.IsPullback m π χ' h.Ω₀.arrow → χ' = h.χ m
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_eq_bot : ∀ {M : Type u_2} [inst : MulOneClass M] {S : Submonoid Mᵐᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t.get! a = t[a]!
-- Mathlib.Algebra.Order.Group.Action.End
RelIso.apply_faithfulSMul : ∀ {α : Type u_1} {r : α → α → Prop}, FaithfulSMul (r ≃r r) α
-- Mathlib.Topology.Defs.Filter
/-- A point `x` is a cluster point of a filter `F` if `𝓝 x ⊓ F ≠ ⊥`.
Also known as an accumulation point or a limit point, but beware that terminology varies.
This is *not* the same as asking `𝓝[≠] x ⊓ F ≠ ⊥`, which is called `AccPt` in Mathlib.
See `mem_closure_iff_clusterPt` in particular.  -/
ClusterPt : {X : Type u_1} → [TopologicalSpace X] → X → Filter X → Prop
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanUnit_app_whiskerLeft_lanAdjunction_counit_app_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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H) {Z : CategoryTheory.Functor C H} (h : L.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.lanUnit.app (L.comp G))
      (CategoryTheory.CategoryStruct.comp (L.whiskerLeft ((L.lanAdjunction H).counit.app G)) h) =
    h
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) (g : β → α) (s : Set β)
  [inst_1 : UniformSpace α],
  HasProdUniformlyOn f g s = HasProd (⇑(UniformOnFun.ofFun {s}) ∘ f) ((UniformOnFun.ofFun {s}) g)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpointType.inductiveFixpoint : Lean.Elab.PartialFixpointType
-- Mathlib.Analysis.Normed.Order.Hom.Basic
AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq : ∀ {F : Type u_1} {α : Type u_2} [inst : FunLike F α ℝ] [inst_1 : AddCommGroup α] [inst_2 : AddGroupSeminormClass F α ℝ]
  (f : F) (x : α), ‖x‖ = f x
-- Init.Data.Float.Model.Float
/-- Converts an `Int64` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofInt64 : Int64 → Float.Model
-- Mathlib.Data.List.TakeWhile
List.find?_eq_head?_dropWhile_not : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.find? p l = (List.dropWhile (fun x => !p x) l).head?
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.deltaLHSUntilFix : Lean.Name → Lean.Name → Lean.MVarId → Lean.MetaM Lean.MVarId