mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.mono_of_isZero_kernel' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  (c : CategoryTheory.Limits.KernelFork f) (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.Limits.IsZero c.pt → CategoryTheory.Mono f
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_pair : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι] {a b : ι},
  a ≠ b → ∏ x ∈ {a, b}, f x = f a * f b
-- Aesop.BuiltinRules.DestructProducts
_private.Aesop.BuiltinRules.DestructProducts.0.Aesop.BuiltinRules.destructProductHyp?.tac : Lean.MVarId →
  Lean.FVarId →
    Lean.Expr →
      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Name → Lean.Name → Lean.MetaM (Lean.MVarId × Lean.Name × Lean.Name)
-- Init.Data.Float.Float
/-- Obtains a `Float` whose value is near the given `USize`.

It will be exactly the value of the given `USize` if such a `Float` exists. If no such `Float`
exists, the returned value will either be the smallest `Float` that is larger than the given value,
or the largest `Float` that is smaller than the given value.

This function has a logical model in terms of `Float.Model`, but is overridden at runtime with an
efficient implementation.
 -/
USize.toFloat : USize → Float
-- Mathlib.RingTheory.Algebraic.Basic
/-- **Alias** of `isAlgebraic_ratCast`. -/
isAlgebraic_rat : ∀ (R : Type u) {A : Type v} [inst : DivisionRing A] [inst_1 : Field R] [inst_2 : Algebra R A] (n : ℚ), IsAlgebraic R ↑n
-- Mathlib.Data.Finset.Union
Finset.biUnion_singleton_eq_self : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], s.biUnion singleton = s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Order.Monotone.Basic
strictAnti_toDual_comp_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti (⇑OrderDual.toDual ∘ f) ↔ StrictMono f
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) (szr : ℕ)
  (k'' : α) (v'' : β k'') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' = Std.DTreeMap.Internal.Impl.leaf →
        motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr_1 : ℕ) →
      (k''_1 : α) →
        (v''_1 : β k''_1) →
          (l''_1 r''_1 : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1).Balanced) →
              Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' =
                  Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1 →
                motive (Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1) hr),
  (match hr' : Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr_1 k''_1 v''_1 l''_1 r''_1, hr => h_2 szr_1 k''_1 v''_1 l''_1 r''_1 hr hr') =
    h_2 szr k'' v'' l'' r'' hr ⋯
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] (x : FreeAddGroup α) (n : ℕ),
  (n • x).toWord = FreeAddGroup.reduce (List.replicate n x.toWord).flatten
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderiv_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E} (n : ℕ),
  DifferentiableAt 𝕜 f x → fderiv 𝕜 (f ^ n) x = (n • f x ^ (n - 1)) • fderiv 𝕜 f x
-- Mathlib.RingTheory.PicardGroup
Submodule.instInvertibleSubtypeMemVal : ∀ {R : Type u} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (I : (Submodule R A)ˣ), Module.Invertible R ↥↑I
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instNonempty : ∀ {M : Type u_1} [Nonempty M], Nonempty (MulArchimedeanOrder M)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algHom_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [IsLocalization M S] [inst_5 : Algebra R P],
  Subsingleton (S →ₐ[R] P)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_inverse_obj_X : ∀ (X : Bipointed), (Bipointed.swapEquiv.inverse.obj X).X = X.X
-- Mathlib.Algebra.Order.Invertible
invOf_pos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  0 < ⅟a ↔ 0 < a
-- Mathlib.Algebra.GroupWithZero.Hom
/-- The proposition that the function preserves multiplication  -/
MonoidWithZeroHom.map_mul' : ∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (self : α →*₀ β) (x y : α),
  (↑self).toFun (x * y) = (↑self).toFun x * (↑self).toFun y
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `lowerBound?` is less or equal to the `cut`.  -/
RBTree.RBNode.lowerBound?_le' : ∀ {α : Type u_1} {lb : Option α} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  (∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt) → RBTree.RBNode.lowerBound? cut t lb = some x → cut x ≠ Ordering.lt
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The right action on objects. This is denoted `d ⊙ᵣ c`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj : {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.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] → D → C → D
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear equivalences.  -/
InnerProductSpace.laplacianWithin_CLE_comp_left : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace ℝ G] {f : E → F} {x : E} {s : Set E} {l : F ≃L[ℝ] G},
  UniqueDiffOn ℝ s →
    x ∈ s → InnerProductSpace.laplacianWithin (⇑l ∘ f) s x = (⇑l ∘ InnerProductSpace.laplacianWithin f s) x
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.mk : ∀ {G : Type u_1} [inst : Group G], commutator G = ⊤ → Group.IsPerfect G
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.setLIntegral_restrict : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
  (κ : ProbabilityTheory.Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ENNReal) (t : Set β),
  ∫⁻ (b : β) in t, f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a
-- Init.Data.SInt.Basic
instSubISize : Sub ISize
-- Init.Data.List.Nat.InsertIdx
List.length_insertIdx_of_le_length : ∀ {α : Type u} {i : ℕ} {as : List α}, i ≤ as.length → ∀ (a : α), (as.insertIdx i a).length = as.length + 1
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
/-- `φ`, `ψ` and `ψ.comp φ` form a `MonoidHom.CompTriple`

(to be used with care, because no simplification is done)  -/
MonoidHom.CompTriple.comp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P}, φ.CompTriple ψ (ψ.comp φ)
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_id : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddZeroClass α],
  (AddMonoidHom.id α).mapMatrix = AddMonoidHom.id (Matrix m n α)
-- Mathlib.Order.ULift
ULift.up_compl : ∀ {α : Type u} [inst : Compl α] (a : α), { down := aᶜ } = { down := a }ᶜ
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.instInhabited : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → Inhabited (N ⋊[φ] G)
-- Mathlib.Order.ModularLattice
/-- **Alias** of `covBy_sup_of_inf_covBy_right`. -/
CovBy.sup_of_inf_right : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α] {a b : α}, a ⊓ b ⋖ b → a ⋖ a ⊔ b
-- Init.Data.String.Extra
String.utf8DecodeChar? : ByteArray → ℕ → Option Char
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_add_edgeDensity_compl : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β},
  s.Nonempty → t.Nonempty → Rel.edgeDensity r s t + Rel.edgeDensity (fun x y => ¬r x y) s t = 1
-- Mathlib.Probability.HasLaw
ProbabilityTheory.hasLaw_dirac_of_ae_eq : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {x : 𝓧},
  (X =ᵐ[P] fun x_1 => x) → ProbabilityTheory.HasLaw X (MeasureTheory.Measure.dirac x) P
-- Mathlib.Order.RelClasses
/-- **Alias** of `Std.Trichotomous.swap`. -/
IsTrichotomous.swap : ∀ {α : Type u} (r : α → α → Prop) [Std.Trichotomous r], Std.Trichotomous (Function.swap r)
-- Mathlib.Algebra.Star.StarAlgHom
/-- A *non-unital ⋆-algebra homomorphism* is a non-unital algebra homomorphism between
non-unital `R`-algebras `A` and `B` equipped with a `star` operation, and this homomorphism is
also `star`-preserving.  -/
«term_→⋆ₙₐ_» : Lean.TrailingParserDescr
-- Mathlib.Data.Ordmap.Invariants
/-- Build a tree from three nodes, with `a () b -> a (() b)` and `a (b c) d -> ((a b) (c d))`.  -/
Ordnode.node4R : {α : Type u_1} → Ordnode α → α → Ordnode α → α → Ordnode α → Ordnode α
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go.eq_def : ∀ {m : Type → Type} {α : Type} [inst : Monad m] [inst_1 : MonadLiftT BaseIO m] (cctx : Lean.Core.Context)
  (env : Lean.Environment)
  (act : Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α)))
  (constantsPerTask n : ℕ) (ngen : Lean.NameGenerator) (tasks : Array (Task (Lean.Meta.LazyDiscrTree.InitResults α)))
  (start cnt idx : ℕ),
  Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go✝ cctx env act constantsPerTask n ngen tasks start cnt idx =
    if h : idx < env.header.moduleData.size then
      have mdata := env.header.moduleData[idx];
      have cnt := cnt + mdata.constants.size;
      if cnt > constantsPerTask then
        match ngen.mkChild with
        | (childNGen, ngen) => do
          let t ←
            liftM (Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq cctx childNGen env act start (idx + 1)).asTask
          Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go✝ cctx env act constantsPerTask n ngen (tasks.push t)
              (idx + 1) 0 (idx + 1)
      else
        Lean.Meta.LazyDiscrTree.createImportedDiscrTree.go✝ cctx env act constantsPerTask n ngen tasks start cnt
          (idx + 1)
    else
      if start < n then
        match ngen.mkChild with
        | (childNGen, snd) => do
          let t ← liftM (Lean.Meta.LazyDiscrTree.createImportedEnvironmentSeq cctx childNGen env act start n).asTask
          pure (tasks.push t)
      else pure tasks
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_measure_of_integrable : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} {μ' : MeasureTheory.Measure α} (c' : ENNReal),
  c' ≠ ⊤ →
    μ' ≤ c' • μ →
      ∀ (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C')
        (f : α → E), MeasureTheory.Integrable f μ → MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' f
-- Init.Data.List.Lemmas
List.filterMap_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → Option γ} {l : List α},
  List.filterMap g (List.filterMap f l) = List.filterMap (fun x => (f x).bind g) l
-- Mathlib.RingTheory.Polynomial.Chebyshev
_private.Mathlib.RingTheory.Polynomial.Chebyshev.0.Polynomial.Chebyshev.T.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : ℕ) → motive (Int.ofNat n.succ.succ)) (h_4 : (n : ℕ) → motive (Int.negSucc n)),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | Int.ofNat n.succ.succ => h_3 n
    | Int.negSucc n => h_4 n) =
    h_2 ()
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Internal.Raw₀.Const.getD (m₁.inter m₂) k fallback =
          if m₂.contains k = true then Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback else fallback
-- Lean.Elab.Term.TermElabM
/-- Metavariable for implicit arguments. `ctx` is the parent application,
`lctx` is a local context where it is valid (necessary for eta feature for named arguments).  -/
Lean.Elab.Term.MVarErrorKind.implicitArg : Lean.LocalContext → Lean.Expr → Lean.Elab.Term.MVarErrorKind
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) {X Y : C}
  (f g : X ⟶ Y) (x : J.R), (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).fst x = f
-- Aesop.Util.UnorderedArraySet
Aesop.UnorderedArraySet.instForInOfMonad : {α : Type u_1} → [inst : BEq α] → {m : Type u_2 → Type u_3} → [Monad m] → ForIn m (Aesop.UnorderedArraySet α) α
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure.neZero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ], NeZero μ
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)) {Z : CommRingCat}
  (h : (AlgebraicGeometry.Spec R).residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).presheaf.germ ⊤ x trivial)
        (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).residue x) h))
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp : CategoryTheory.ConcreteCategory FiniteGrp.{u_1} fun x1 x2 => ↑x1.toGrp →* ↑x2.toGrp
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- If `h : P ≤ P'` is an inequality of properties of objects,
this is the obvious isomorphism `ιOfLE h ⋙ P'.ι ≅ P.ι`.  -/
CategoryTheory.ObjectProperty.ιOfLECompιIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P P' : CategoryTheory.ObjectProperty C} → (h : P ≤ P') → (CategoryTheory.ObjectProperty.ιOfLE h).comp P'.ι ≅ P.ι
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ β) (h1 : Measurable ⇑e)
  (h2 : Measurable ⇑e.symm), ⇑{ toEquiv := e, measurable_toFun := h1, measurable_invFun := h2 } = ⇑e
-- Mathlib.Computability.Encoding
Computability.Γ'.ket.sizeOf_spec : sizeOf Computability.Γ'.ket = 1
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  (X : HomotopicalAlgebra.FibrantObject C),
  HomotopicalAlgebra.IsFibrant ((HomotopicalAlgebra.FibrantObject.localizerMorphism C).functor.obj X)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Proper group action in the sense of Bourbaki:
the map `G × X → X × X` is a proper map (see `IsProperMap`).  -/
ProperSMul.isProperMap_smul_pair : ∀ {G : Type u_1} {X : Type u_2} {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : Group G}
  {inst_3 : MulAction G X} [self : ProperSMul G X], IsProperMap fun gx => (gx.1 • gx.2, gx.2)
-- Mathlib.Data.Set.Finite.Basic
/-- Note that this is an equality of types not holding definitionally. Use wisely.  -/
Set.Finite.coeSort_toFinset : ∀ {α : Type u} {s : Set α} (hs : s.Finite), ↥hs.toFinset = ↑s
-- Mathlib.Topology.UniformSpace.AbsoluteValue
/-- The uniform structure coming from an absolute value.  -/
AbsoluteValue.uniformSpace : {𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [IsStrictOrderedRing 𝕜] → {R : Type u_2} → [inst_3 : CommRing R] → AbsoluteValue R 𝕜 → UniformSpace R
-- Mathlib.Data.EReal.Basic
/-- A recursor for `EReal` in terms of the coercion.

When working in term mode, note that pattern matching can be used directly,
although this is prone to leaking the implementation details in terms of `Option`.  -/
EReal.rec : {motive : EReal → Sort u_1} → motive ⊥ → ((a : ℝ) → motive ↑a) → motive ⊤ → (a : EReal) → motive a
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Every presheaf is a sheaf for the maximal sieve.

[Elephant] C2.1.5(ii)
 -/
CategoryTheory.Presieve.isSheafFor_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor P ⊤
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_unitIso : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))).obj
            x))
      ⋯
-- Mathlib.Data.Set.PowersetCard
/-- The map `powersetCard α n → powersetCard β n` induced by embedding `f : α ↪ β`.  -/
Set.powersetCard.map : {α : Type u_1} → (n : ℕ) → {β : Type u_2} → (α ↪ β) → ↑(Set.powersetCard α n) → ↑(Set.powersetCard β n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CartesianMonoidalCategory.lift f g) h)
      (CategoryTheory.MonoidalCategoryStruct.associator Y Z W).hom =
    CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CartesianMonoidalCategory.lift g h)
-- Mathlib.Order.Cover
WithTop.coe_wcovBy_top : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ↑a ⩿ ⊤ ↔ IsMax a
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The bijection between the free group on the empty type, and a type with one element.  -/
FreeGroup.freeGroupEmptyEquivUnit : FreeGroup Empty ≃ Unit
-- Mathlib.Algebra.Lie.Classical
/-- The indefinite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric
bilinear form defined by the indefinite diagonal matrix.  -/
LieAlgebra.Orthogonal.so' : (p : Type u_2) →
  (q : Type u_3) →
    (R : Type u₂) →
      [inst : DecidableEq p] →
        [inst_1 : DecidableEq q] →
          [inst_2 : CommRing R] →
            [inst_3 : Fintype p] → [inst_4 : Fintype q] → LieSubalgebra R (Matrix (p ⊕ q) (p ⊕ q) R)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (toIntInst rangeExpr : Lean.Expr)
  (range : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval) (toInt wrap : Lean.Expr) (ofWrap0? : Option Lean.Expr)
  (ofEq ofDiseq : Lean.Expr) (lowerThm? upperThm? : Option Lean.Expr)
  (ofLE? ofNotLE? ofLT? ofNotLT? : Option (Option Lean.Expr))
  (addThms? mulThms? : Option Lean.Meta.Grind.Arith.Cutsat.ToIntThms)
  (subThm? negThm? divThm? modThm? powThm? zeroThm? ofNatThm? : Option (Option Lean.Expr)),
  sizeOf
      { id := id, type := type, u := u, toIntInst := toIntInst, rangeExpr := rangeExpr, range := range, toInt := toInt,
        wrap := wrap, ofWrap0? := ofWrap0?, ofEq := ofEq, ofDiseq := ofDiseq, lowerThm? := lowerThm?,
        upperThm? := upperThm?, ofLE? := ofLE?, ofNotLE? := ofNotLE?, ofLT? := ofLT?, ofNotLT? := ofNotLT?,
        addThms? := addThms?, mulThms? := mulThms?, subThm? := subThm?, negThm? := negThm?, divThm? := divThm?,
        modThm? := modThm?, powThm? := powThm?, zeroThm? := zeroThm?, ofNatThm? := ofNatThm? } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf toIntInst + sizeOf rangeExpr + sizeOf range + sizeOf toInt +
                                          sizeOf wrap +
                                        sizeOf ofWrap0? +
                                      sizeOf ofEq +
                                    sizeOf ofDiseq +
                                  sizeOf lowerThm? +
                                sizeOf upperThm? +
                              sizeOf ofLE? +
                            sizeOf ofNotLE? +
                          sizeOf ofLT? +
                        sizeOf ofNotLT? +
                      sizeOf addThms? +
                    sizeOf mulThms? +
                  sizeOf subThm? +
                sizeOf negThm? +
              sizeOf divThm? +
            sizeOf modThm? +
          sizeOf powThm? +
        sizeOf zeroThm? +
      sizeOf ofNatThm?
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.L₀.g S.δ = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ},
  Std.DTreeMap.Const.getD (Std.DTreeMap.map f t) k fallback =
    (Option.map (f k) (Std.DTreeMap.Const.get? t k)).getD fallback
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.addCommMonoid : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₂ M₂] → [ContinuousAdd M₂] → AddCommMonoid (M₁ →SL[σ₁₂] M₂)