mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.funLike : {R : Type u_1} → [inst : NonUnitalRing R] → FunLike (RingSeminorm R) R ℝ
-- Init.Data.List.Attach
List.foldl_attachWith : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {q : α → Prop} (H : ∀ a ∈ l, q a) {f : β → { x // q x } → β} {b : β},
  List.foldl f b (l.attachWith q H) =
    List.foldl
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach
-- Mathlib.Topology.Category.UniformSpace
/-- The forgetful functor from uniform spaces to topological spaces.  -/
UniformSpaceCat.hasForgetToTop : CategoryTheory.HasForget₂ UniformSpaceCat TopCat
-- Mathlib.Probability.Kernel.CondDistrib
/-- The conditional expectation of a function `f` of the product `(X, Y)` is almost everywhere equal
to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel.  -/
ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F] [CompleteSpace F],
  Measurable X →
    AEMeasurable Y μ →
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.Integrable (fun a => f (X a, Y a)) μ →
          μ[fun a => f (X a, Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a =>
            ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.forInUncurried_eq_forIn_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Const.forInUncurried f init t = forIn (Std.DTreeMap.Const.toList t) init f
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsInduced.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂},
  W₂.inverseImage Φ.functor = W₁ → Φ.IsInduced
-- Mathlib.SetTheory.Cardinal.Regular
Ordinal.omega_univ : Ordinal.omega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}
-- Mathlib.LinearAlgebra.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {n : Type u_3}
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R V) (g : SpecialLinearGroup R V),
  ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = (LinearMap.toMatrix b b) ↑↑g
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The coefficients `M →₀ R` of an element of the monoid algebra `R[M]`.  -/
MonoidAlgebra.coeff : {R : Type u_8} → {M : Type u_9} → [inst : Semiring R] → MonoidAlgebra R M → M →₀ R
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is an `AddMonoid` under pointwise operations if `α` is.  -/
Set.addMonoid : {α : Type u_2} → [AddMonoid α] → AddMonoid (Set α)
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView.mk.inj : ∀ {module? module?_1 : Option Lean.DeclarationLocation},
  { module? := module? } = { module? := module?_1 } → module? = module?_1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
_private.Mathlib.Topology.ContinuousMap.Bounded.Normed.0.zpowRec.match_1.eq_1 : ∀ {G : Type u_2} (motive : ℤ → G → Sort u_1) (n : ℕ) (a : G) (h_1 : (n : ℕ) → (a : G) → motive (Int.ofNat n) a)
  (h_2 : (n : ℕ) → (a : G) → motive (Int.negSucc n) a),
  (match Int.ofNat n, a with
    | Int.ofNat n, a => h_1 n a
    | Int.negSucc n, a => h_2 n a) =
    h_1 n a
-- Mathlib.RingTheory.Ideal.Basis
Ideal.basisSpanSingleton.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (b b_1 : Module.Basis ι R S),
  b = b_1 → ∀ {x : S} (hx : x ≠ 0), Ideal.basisSpanSingleton b hx = Ideal.basisSpanSingleton b_1 hx
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.tanh_half_dist : ∀ (z w : UpperHalfPlane), Real.tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)
-- Mathlib.Data.Set.Image
Set.preimage_id : ∀ {α : Type u_1} {s : Set α}, id ⁻¹' s = s
-- Mathlib.MeasureTheory.Constructions.Projective
MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)]
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)},
  MeasureTheory.IsProjectiveMeasureFamily P → ∀ (I J : Finset ι), (P I) Set.univ = (P J) Set.univ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.snd_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.AddGrp C),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd G H).hom.hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd G.X H.X
-- Mathlib.Lean.Meta
/-- Add the hypothesis `h : t`, given `v : t`, and return the new `FVarId`.  -/
Lean.MVarId.let : Lean.MVarId → Lean.Name → Lean.Expr → optParam (Option Lean.Expr) none → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- The C⋆-algebra-valued Cauchy-Schwarz inequality for Hilbert C⋆-modules.  -/
CStarModule.inner_mul_inner_swap_le : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : Norm E] [inst_6 : CStarModule A E] [StarOrderedRing A] {x y : E},
  inner A x y * inner A y x ≤ ‖x‖ ^ 2 • inner A y y
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSubNegAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubNegMonoid α],
  Lex.instSubNegAddMonoid =
    { toAddMonoid := Lex.instAddMonoid, toNeg := Lex.instNeg, toSub := Lex.instSub, toZSMul := ZSMul.ofSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_nil : ∀ (τ : Type u), Function.FromTypes ![] τ = τ
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.instBEqErrorFormat : BEq Mathlib.Linter.TextBased.ErrorFormat
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `(F ⋙ forget CommSemiRingCat).sections` is `u`-small, `F` has a limit.  -/
CommSemiRingCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommSemiRingCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- We define `Gᶜ` to be the `SimpleGraph V` such that no two adjacent vertices in `G`
are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
(still ensuring that vertices are not adjacent to themselves).  -/
SimpleGraph.instCompl : {V : Type u} → Compl (SimpleGraph V)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- If `f : E ⟶ F` and `g : F ⟶ E` are refinement morphisms of pre-`1`-hypercovers such that
the composition `g ≫ f` is homotopic to the identity, then if the multifork associated
to `E` is exact also the multifork associated to `F` is exact.  -/
CategoryTheory.PreOneHypercover.Homotopy.isLimitMultifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {A : Type u_1} →
            [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
              (f : E.Hom F) →
                (g : F.Hom E) →
                  CategoryTheory.PreOneHypercover.Homotopy (g.comp f) (CategoryTheory.PreOneHypercover.Hom.id F) →
                    {G : CategoryTheory.Functor Cᵒᵖ A} →
                      CategoryTheory.Limits.IsLimit (E.multifork G) → CategoryTheory.Limits.IsLimit (F.multifork G)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.modify.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {β : Type v}
  (m m_1 : Std.ExtDHashMap α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : β → β), f = f_1 → Std.ExtDHashMap.Const.modify m a f = Std.ExtDHashMap.Const.modify m_1 a_1 f_1
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_mul_left_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulLeftInvariant] (x : G), Filter.map (fun h => x * h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMinOrderElemIic : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMinOrder α], NoMinOrder ↑(Set.Iic a)
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.Epi.hcongr_5 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' →
            ∀ (Y : C) (Y' : C'),
              Y ≍ Y' → ∀ (f : X ⟶ Y) (f' : X' ⟶ Y'), f ≍ f' → CategoryTheory.Epi f ≍ CategoryTheory.Epi f'
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatDecl : Std.ToFormat Lean.IR.Decl
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.ne : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) (x : ↑P.I) (y : ↑P.II), ↑x ≠ ↑y
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G),
  (3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
    ∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
      (∀ (i : ι), (X i).Nonempty) →
        Pairwise (Function.onFun Disjoint X) →
          (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
            ∀ [Nontrivial ι] {i j : ι} (w : Monoid.CoprodI.NeWord H i j), (Monoid.CoprodI.lift f) w.prod ≠ 1
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunAlgHom_apply_tmul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R),
  (PolyEquivTensor.toFunAlgHom R A) (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rcc_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toList.getD i fallback = m + ↑i
-- Mathlib.Order.Interval.Finset.Basic
Finset.right_mem_Ioc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ∈ Finset.Ioc a b ↔ a < b
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.testBit.match_1.splitter : (motive : ℤ → ℕ → Sort u_1) →
  (x : ℤ) → (x_1 : ℕ) → ((m n : ℕ) → motive (Int.ofNat m) n) → ((m n : ℕ) → motive (Int.negSucc m) n) → motive x x_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sinh_sub_pi_mul_I : ∀ (z : ℂ), Complex.sinh (z - ↑Real.pi * Complex.I) = -Complex.sinh z
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A natural isomorphism between the functor `map (F ⋙ G) ` and `map F ⋙ map G `.  -/
CategoryTheory.WithTerminal.mapComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      {E : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.Category.{v_2, u_2} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                CategoryTheory.WithTerminal.map (F.comp G) ≅
                  (CategoryTheory.WithTerminal.map F).comp (CategoryTheory.WithTerminal.map G)
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given a `LawfulUpwardEnumerable` instance.
 -/
Std.Roi.isEmpty : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Roi α → Bool
-- Mathlib.Analysis.Calculus.Taylor
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.

Version for open intervals  -/
taylorWithinEval_hasDerivAt_Ioo : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ},
  a < b →
    t ∈ Set.Ioo a b →
      ContDiffOn ℝ (↑n) f (Set.Icc a b) →
        DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Ioo a b) →
          HasDerivAt (fun y => taylorWithinEval f n (Set.Icc a b) y x)
            (((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) t
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.desc.congr_simp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {X : C} (f f_1 : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (e_f : f = f_1)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)),
  CategoryTheory.Limits.chosenCoend.desc f hf = CategoryTheory.Limits.chosenCoend.desc f_1 ⋯
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ExprConfigCacheKey.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (configKey : UInt64),
  sizeOf { expr := expr, configKey := configKey } = 1 + sizeOf expr + sizeOf configKey
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  [inst_7 : Algebra.FormallyEtale S T] (x : TensorProduct S T Ω[S⁄R]),
  (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R S T) x = (KaehlerDifferential.mapBaseChange R S T) x
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), s ∪ s = s
-- Aesop.Builder.Basic
Aesop.RuleBuilderOptions.immediatePremises? : Aesop.RuleBuilderOptions → Option (Array Lean.Name)
-- Std.Data.Iterators.Combinators.Monadic.Drop
/-- The internal state of the `IterM.drop` combinator.
 -/
Std.Iterators.Types.Drop : Type w → (Type w → Type w') → Type w → Type w
-- Lean.Syntax
Lean.Syntax.getRangeWithTrailing? : Lean.Syntax → optParam Bool false → Option Lean.Syntax.Range
-- Init.Data.String.Basic
String.Slice.Pos.prevAux_lt_self : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prevAux h < p.offset
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ioi_sub_one_eq_Ici : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderTop α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (a : α), Finset.Ioi (a - 1) = Finset.Ici a
-- Lean.Parser.Basic
Lean.Parser.checkLineEqFn : String → Lean.Parser.ParserFn
-- Mathlib.Data.Part
Part.mem_restrict : ∀ {α : Type u_1} (p : Prop) (o : Part α) (h : p → o.Dom) (a : α), a ∈ Part.restrict p o h ↔ p ∧ a ∈ o
-- Batteries.Data.BitVec.Basic
/-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian.  -/
BitVec.ofFnLEAux : {n : ℕ} → (m : ℕ) → (Fin n → Bool) → BitVec m
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_hom_rel : ∀ {ι : Type u_2} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Multiset ι)
  {r : M → N → Prop} {f : ι → M} {g : ι → N},
  r 0 0 → (∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a + b) (g a + c)) → r (Multiset.map f s).sum (Multiset.map g s).sum
-- Batteries.Data.List.Basic
List.swapTR.go.eq_5 : ∀ {α : Type u_1} (l : List α) (a : Array α) (a_1 : α) (xs : List α) (i j : ℕ),
  List.swapTR.go l (a_1 :: xs) i.succ j.succ a = List.swapTR.go l xs i j (a.push a_1)
-- Lean.Parser.Term
Lean.Parser.Term.letPosOpt : Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- For nonempty `α`, `least?` has a value and every other value is a transitive successor of it.  -/
Std.PRange.LawfulUpwardEnumerableLeast?.least?_le : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.Least? α}
  [self : Std.PRange.LawfulUpwardEnumerableLeast? α] (a : α),
  ∃ init, Std.PRange.least? = some init ∧ Std.PRange.UpwardEnumerable.LE init a
-- Lean.Parser.Term
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.  -/
Lean.Parser.Term.type : Lean.Parser.Parser
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Hom.hom₂_ofHom₂ : ∀ {R : Type u_1} [inst : CommRing R] {M N P : ModuleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P),
  ModuleCat.Hom.hom₂ (ModuleCat.ofHom₂ f) = f
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.mk : ∀ {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 : D), CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow F X)) → CategoryTheory.RepresentablyCoflat F
-- Init.Data.List.Lemmas
List.set_eq_of_length_le : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.length ≤ i → ∀ {a : α}, l.set i a = l
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, (t₁ \ t₂).getKey! k = if k ∈ t₂ then default else t₁.getKey! k
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKeyD fallback = t₂.minKeyD fallback
-- Mathlib.Data.ENat.Basic
ENat.map_natCast : ∀ {α : Type u_1} (f : ℕ → α) (a : ℕ), ENat.map f ↑a = ↑(f a)
-- Init.Core
/-- Extracts a squashed value into any subsingleton type.

If `β` is a subsingleton, a function `α → β` cannot distinguish between elements of `α` and thus
automatically respects the universal relation that `Squash` quotients with.
 -/
Squash.lift : {α : Sort u_1} → {β : Sort u_2} → [Subsingleton β] → Squash α → (α → β) → β
-- Mathlib.Logic.ExistsUnique
ExistsUnique.choose_eq_iff : ∀ {α : Sort u_1} {p : α → Prop} {a : α} (h : ∃! x, p x), Exists.choose h = a ↔ p a
-- Mathlib.Algebra.Star.MonoidHom
/-- Copy of a `StarMonoidHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
StarMonoidHom.copy : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Star A] → [inst_2 : Monoid B] → [inst_3 : Star B] → (f : A →⋆* B) → (f' : A → B) → f' = ⇑f → A →⋆* B
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toCharThreeNF.eq_1 : ∀ {F : Type u_2} [inst : Field F] [inst_1 : CharP F 3] (W : WeierstrassCurve F),
  W.toCharThreeNF =
    { u := 1, r := (W.toShortNFOfCharThree • W).a₄ / (W.toShortNFOfCharThree • W).a₂, s := 0, t := 0 } *
      W.toShortNFOfCharThree
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.mk : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId → Lean.Name → Lean.Expr → Lean.Compiler.LCNF.LetValue pu → Lean.Compiler.LCNF.LetDecl pu
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSubNegAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubNegMonoid α],
  Colex.instSubNegAddMonoid =
    { toAddMonoid := Colex.instAddMonoid, toNeg := Colex.instNeg, toSub := Colex.instSub, toZSMul := ZSMul.ofSMul,
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Lean.Meta.Instances
Lean.Meta.getInstancePriority? : Lean.Name → Lean.CoreM (Option ℕ)
-- Batteries.Data.UInt
UInt16.max_def : ∀ (x y : UInt16), x ⊔ y = if x ≤ y then y else x
-- Mathlib.Algebra.Group.Equiv.Defs
/-- `MulEquivClass F A B` states that `F` is a type of multiplication-preserving morphisms.
You should extend this class when you extend `MulEquiv`.  -/
MulEquivClass : (F : Type u_9) → (A : outParam (Type u_10)) → (B : outParam (Type u_11)) → [Mul A] → [Mul B] → [EquivLike F A B] → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_le_size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.size ≤ (t.insertMany l).size
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_map : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N'] (f : M →ₗ[R] M')
  (g : N →ₗ[R] N'),
  ↑(TensorProduct.comm R M' N') ∘ₗ TensorProduct.map f g = TensorProduct.map g f ∘ₗ ↑(TensorProduct.comm R M N)
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.instIsProbabilityMeasureMapNatCastPoissonMeasure : ∀ (r : NNReal) {R : Type u_1} [inst : NatCast R] [inst_1 : MeasurableSpace R],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r))
-- Mathlib.NumberTheory.NumberField.CMField
/-- A nontrivial cyclotomic extension of `ℚ` is CM.
 -/
IsCyclotomicExtension.Rat.isCMField : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] {S : Set ℕ},
  (∃ n ∈ S, 2 < n) → ∀ [IsCyclotomicExtension S ℚ K], NumberField.IsCMField K
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s₀_comp_δ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) {Z : C} (h : X.left.obj (Opposite.op { len := 0 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.s 0) (CategoryTheory.CategoryStruct.comp (X.left.δ 1) h) =
    CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 }))
      (CategoryTheory.CategoryStruct.comp self.s' h)
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- **Alias** of the reverse direction of `AddSubmonoid.saturation_le_iff_le`. -/
AddSubmonoid.saturation_le_of_le : ∀ {M : Type u_1} [inst : AddZeroClass M] {a : AddSubmonoid M} {b : SaturatedAddSubmonoid M},
  a ≤ b.toAddSubmonoid → a.saturation ≤ b
-- Std.Async.Timer
/-- `Interval` can be used to repeatedly wait for some duration like a clock.
The underlying timer has millisecond resolution.
 -/
Std.Async.Interval : Type
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  ↑(HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.spectralObject_ω₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (X : C),
  (t.spectralObject X).ω₁ = t.ω₁.comp ((CategoryTheory.evaluation C C).obj X)
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.free_map_coe : ∀ {α β : Type u} {f : α ⟶ β} (x : FreeAbelianGroup α),
  (CategoryTheory.ConcreteCategory.hom (AddCommGrpCat.free.map f)) x = ⇑(CategoryTheory.ConcreteCategory.hom f) <$> x
-- Init.Control.Lawful.Instances
EStateM.run_get : ∀ {σ ε : Type u_1} (s : σ), get.run s = EStateM.Result.ok s s
-- Init.System.ST
instInhabitedEST : {ε σ α : Type} → [Inhabited ε] → Inhabited (EST ε σ α)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedElimInfo.default : Lean.Meta.ElimInfo