mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → ∀ {fallback : α}, Std.Internal.List.containsKey (Std.Internal.List.maxKeyD l fallback) l = true
-- Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
/-- Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite
measure and `f` is an almost everywhere measurable function that is continuous at a point `a`, then
`∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s` tends to
`(𝓝 a).smallSets` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `μ.real (s i)` in
the actual statement.

Often there is a good formula for `μ.real (s i)`, so the formalization can take an optional
argument `m` with this formula and a proof of `(fun i => μ.real (s i)) =ᶠ[li] m`. Without these
arguments, `m i = μ.real (s i)` is used in the output.  -/
ContinuousAt.integral_sub_linear_isLittleO_ae : ∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {f : X → E},
  ContinuousAt f x →
    StronglyMeasurableAtFilter f (nhds x) μ →
      ∀ {s : ι → Set X} {li : Filter ι},
        Filter.Tendsto s li (nhds x).smallSets →
          ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
            autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousAt.integral_sub_linear_isLittleO_ae._auto_1 →
              (fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.toIsSeparated : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsProper f], AlgebraicGeometry.IsSeparated f
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The type of natural transformations `shrinkCoyoneda.{w}.obj X ⟶ P`
with `X : Cᵒᵖ` and `P : C ⥤ Type w` is equivalent to `P.obj (op X)`.  -/
CategoryTheory.shrinkCoyonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
      {X : Cᵒᵖ} →
        {P : CategoryTheory.Functor C (Type w)} →
          (CategoryTheory.shrinkCoyoneda.{w, v, u}.obj X ⟶ P) ≃ P.obj (Opposite.unop X)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty : {α : Type u} → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
-- Mathlib.Order.Antichain
/-- **Alias** of `setOfPred_minimal_antichain`. -/
setOf_minimal_antichain : ∀ {α : Type u_1} [inst : PartialOrder α] (P : α → Prop), IsAntichain (fun x1 x2 => x1 ≤ x2) {x | Minimal P x}
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.instNeZeroNatTorsionOrder : ∀ (K : Type u_1) [inst : Field K] [NumberField K], NeZero (NumberField.Units.torsionOrder K)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  AddSubgroup.centralizer s = { toAddSubmonoid := AddSubmonoid.centralizer s, neg_mem' := ⋯ }
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_eq_of_inf_eq : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B C : IntermediateField F E},
  A ⊓ C = B ⊓ C → A.relrank C = B.relrank C
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coe_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N) (g : M →+ P), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.of_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {X Y : C} (e : X ≅ Y),
  P.limitsClosure J X → P.limitsClosure J Y
-- Std.Data.TreeMap.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.TreeMap.keyAtIdx? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → ℕ → Option α
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_left : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 cnf3 : Std.Sat.CNF ℕ} {new1 : ℕ} {hnew1 : new1 < aig.decls.size} {new2 : ℕ}
  {hnew2 : new2 < aig.decls.size} (cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1)
  (cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2) (cache3 : Std.Sat.AIG.toCNF.Cache✝ aig cnf3),
  Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 new1 hnew1 →
    Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache2 cache3 new2 hnew2 →
      Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache3 new1 hnew1
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTransposeRingEquiv_symm_apply : ∀ (m : Type u_2) (α : Type v) [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  (a : (Matrix m m α)ᵐᵒᵖ), (Matrix.conjTransposeRingEquiv m α).symm a = (MulOpposite.unop a).conjTranspose
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (f : E ≅ F),
  (CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso f).inverse =
    CategoryTheory.PreOneHypercover.Hom.mapMulticospan f.inv
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toOrderIso_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.toOrderIso = ↑f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instSymmetricCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C],
  CategoryTheory.Mon.instSymmetricCategory =
    { braiding := fun X Y => CategoryTheory.Mon.mkIso' (β_ X.X Y.X), braiding_naturality_right := ⋯,
      braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯, symmetry := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_inv : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] (f : ι → G₀),
  (Function.support fun a => (f a)⁻¹) = Function.support f
-- Mathlib.Algebra.Category.Ring.Basic
/-- The forgetful functor from `RingCat` to `SemiRingCat` is fully faithful.  -/
RingCat.fullyFaithfulForget₂ToSemiRingCat : (CategoryTheory.forget₂ RingCat SemiRingCat).FullyFaithful
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationLeftAdjoint_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) {x d₂ : D} (f : x ⟶ d₂)
  (x_1 : C),
  ((CategoryTheory.evaluationLeftAdjoint D c).map f).app x_1 =
    CategoryTheory.Limits.Sigma.desc fun h =>
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Sigma.ι (fun x => d₂) h)
-- Mathlib.Util.Notation3
/-- Get the accumulated array of delaborated terms for a given foldr/foldl.
Returns `#[]` if nothing has been pushed yet.  -/
Mathlib.Notation3.MatchState.getBinders : Mathlib.Notation3.MatchState → Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_graph_snd_inj' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x y : E × F},
  x ∈ f.graph → y ∈ f.graph → x.1 = y.1 → x.2 = y.2
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.box_upper : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (ν : ι → ℤ),
  (BoxIntegral.unitPartition.box n ν).upper = fun i => (↑(ν i) + 1) / ↑n
-- Mathlib.Data.Int.Bitwise
Int.testBit_land : ∀ (m n : ℤ) (k : ℕ), (m.land n).testBit k = (m.testBit k && n.testBit k)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity).  -/
ContinuousLinearMap.toLinearMap₁₂ : {R : Type u_1} →
  {𝕜₂ : Type u_3} →
    {𝕜₃ : Type u_4} →
      {E : Type u_5} →
        {F : Type u_6} →
          {G : Type u_7} →
            [inst : Semiring R] →
              [inst_1 : NormedField 𝕜₂] →
                [inst_2 : NormedField 𝕜₃] →
                  [inst_3 : AddCommMonoid E] →
                    [inst_4 : Module R E] →
                      [inst_5 : TopologicalSpace E] →
                        [inst_6 : AddCommGroup F] →
                          [inst_7 : Module 𝕜₂ F] →
                            [inst_8 : TopologicalSpace F] →
                              [inst_9 : AddCommGroup G] →
                                [inst_10 : Module 𝕜₃ G] →
                                  [inst_11 : TopologicalSpace G] →
                                    [inst_12 : IsTopologicalAddGroup G] →
                                      [inst_13 : ContinuousConstSMul 𝕜₃ G] →
                                        {σ₁₃ : R →+* 𝕜₃} →
                                          {σ₂₃ : 𝕜₂ →+* 𝕜₃} → (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.smul_posPart : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal),
  (r • j).posPart = r • j.posPart
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore_toDigitsCore : ∀ {b n d fuel nf df : ℕ} {cs : List Char},
  1 < b →
    0 < n →
      d < b →
        b * n + d < fuel →
          n < nf → d < df → b.toDigitsCore nf n (b.toDigitsCore df d cs) = b.toDigitsCore fuel (b * n + d) cs
-- Mathlib.Data.Real.Basic
Real.mk_zero : Real.mk 0 = 0
-- Batteries.Data.List.Perm
List.Perm.union : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ t₁ t₂ : List α}, l₁.Perm l₂ → t₁.Perm t₂ → (l₁ ∪ t₁).Perm (l₂ ∪ t₂)
-- Init.Data.Option.Basic
Option.instMax : {α : Type u_1} → [Max α] → Max (Option α)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_ciInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] (e : α ≃o β) {f : ι → α},
  BddBelow (Set.range f) → e (⨅ i, f i) = ⨅ i, e (f i)
-- Std.Http.Data.Body.Full
_private.Std.Http.Data.Body.Full.0.Std.Http.Body.Full.mk.inj : ∀ {state state_1 : Std.Mutex (Option ByteArray)}, { state := state } = { state := state_1 } → state = state_1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_union_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∪ m₂).getKey? k = m₁.getKey? k
-- Lean.CoreM
/-- Message log.  -/
Lean.Core.State.messages : Lean.Core.State → Lean.MessageLog
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.equalizer_ι_isLocalHom' : ∀ (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPairᵒᵖ CommRingCat),
  IsLocalHom
    (CommRingCat.Hom.hom (CategoryTheory.Limits.limit.π F (Opposite.op CategoryTheory.Limits.WalkingParallelPair.one)))
-- Init.Data.List.Lemmas
List.reflBEq_iff : ∀ {α : Type u_1} [inst : BEq α], ReflBEq (List α) ↔ ReflBEq α
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) (j : J) {Z : C}
  (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv
      (CategoryTheory.CategoryStruct.comp (s.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.CategoryStruct.comp (w.inv.app j) h)
-- Mathlib.Analysis.Convex.Function
/-- A function `-f` is strictly convex iff `f` is strictly concave.  -/
neg_strictConvexOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true
-- Init.Grind.AC
Lean.Grind.AC.Seq.endsWithVar_k_var : ∀ (y x : Lean.Grind.AC.Var), (Lean.Grind.AC.Seq.var y).endsWithVar_k x = (x == y)
-- Aesop.Util.Basic
Aesop.SimpTheorems.foldSimpEntries : {σ : Type u_1} → (σ → Lean.Meta.SimpEntry → σ) → σ → Lean.Meta.SimpTheorems → σ
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.ramificationIdx_le_finrank : ∀ {R : Type u} [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  (K : Type u_1) (L : Type u_2) [inst_4 : Field K] [inst_5 : Field L] [IsDedekindDomain R] [inst_7 : Algebra R K]
  [IsFractionRing R K] [inst_9 : Algebra S L] [IsFractionRing S L] [inst_11 : Algebra K L] [inst_12 : Algebra R L]
  [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S] [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal]
  (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p], p.ramificationIdx' P ≤ Module.finrank K L
-- Mathlib.Algebra.Lie.Classical
/-- A matrix defining a canonical even-rank symmetric bilinear form.

It looks like this as a `2l x 2l` matrix of `l x l` blocks:

```
[ 0 1 ]
[ 1 0 ]
```
 -/
LieAlgebra.Orthogonal.JD : (l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (l ⊕ l) (l ⊕ l) R
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.MemLp.locallyIntegrable : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ]
  {p : ENNReal}, MeasureTheory.MemLp f p μ → 1 ≤ p → MeasureTheory.LocallyIntegrable f μ
-- Mathlib.Computability.EpsilonNFA
/-- `M.stepSet S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`.  -/
εNFA.stepSet : {α : Type u} → {σ : Type v} → εNFA α σ → Set σ → α → Set σ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_comp_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((f ⊓ g).ofLE g ⋯) (CategoryTheory.CategoryStruct.comp g.arrow h) =
    CategoryTheory.CategoryStruct.comp (f ⊓ g).arrow h
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_of_equivalence : ∀ {C : Type u_1} {D : Type u_2} {D' : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} D']
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] (L : CategoryTheory.Functor C D) (L' : CategoryTheory.Functor C D')
  (F : CategoryTheory.Functor C H) (E : D ≌ D') (eL : L.comp E.functor ≅ L') (Y : D) (Y' : D')
  (e : E.functor.obj Y ≅ Y') [L.HasPointwiseRightKanExtensionAt F Y], L'.HasPointwiseRightKanExtensionAt F Y'
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.push.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf σ] (a : σ → Γ k), sizeOf (Turing.TM2to1.StAct.push a) = 1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_or_elim_l : ∀ {σs : List (Type u)} {P Q R T : Std.Do.SPred σs}, (P ∧ R ⊢ₛ T) → (Q ∧ R ⊢ₛ T) → (P ∨ Q) ∧ R ⊢ₛ T
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_sub_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- A continuous function from an `OpensMeasurableSpace` to a `BorelSpace`
is measurable.  -/
Continuous.measurable : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] {f : α → γ}, Continuous f → Measurable f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.ExtDHashMap.map f m},
  (Std.ExtDHashMap.map f m).get k h' = f k (m.get k ⋯)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_obj_eq_as : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I),
  (CategoryTheory.Discrete.functor F).obj X = F X.as
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.add_right_eq_self : ∀ {w : ℕ} (a b : BitVec w), (a + b == a) = (b == 0#w)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.isLeftAdjoint_post : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.IsLeftAdjoint], (CategoryTheory.Under.post F).IsLeftAdjoint
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isPreconnected_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : TopologicalSpace.Compacts α},
  IsPreconnected ↑L → IsPreconnected (Set.Ioc K L)
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_fmod_self_left : ∀ (a b c : ℤ), (a + -(b * c)).fmod b = a.fmod b
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_mul_ne_top : ∀ (a : ENNReal), a⁻¹ * a ≠ ⊤
-- Std.Sync.Semaphore
/-- Creates a resolved promise.
 -/
_private.Std.Sync.Semaphore.0.Std.mkResolvedPromise : {α : Type} → [Nonempty α] → α → BaseIO (IO.Promise α)
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
/-- Summing an indicator function over a possibly larger `Finset` is the same as
summing the original function over the original finset.  -/
Finset.sum_indicator_subset : ∀ {ι : Type u_1} {β : Type u_4} [inst : AddCommMonoid β] (f : ι → β) {s t : Finset ι},
  s ⊆ t → ∑ i ∈ t, (↑s).indicator f i = ∑ i ∈ s, f i
-- Mathlib.Order.Hom.Lattice
SupHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β)
  (map_sup' : ∀ (a b : α), toFun (a ⊔ b) = toFun a ⊔ toFun b), sizeOf { toFun := toFun, map_sup' := map_sup' } = 1
-- Mathlib.Algebra.Order.Kleene
/-- Notation typeclass for the Kleene star `∗`.  -/
KStar : Type u_5 → Type u_5
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.instCovariantClassHSMulLe : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R],
  CovariantClass M (Subring R) HSMul.hSMul LE.le
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State : Type
-- Mathlib.LinearAlgebra.Dimension.Constructions
lift_rank_add_lift_rank_le_rank_prod : ∀ (R : Type u) (M : Type v) (M' : Type v') [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [Nontrivial R],
  Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_embDomain_subset : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R}, (HahnSeries.embDomain f x).support ⊆ ⇑f '' x.support
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T U V W : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct U W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct T V]
  (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {Z : C} (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map h k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp h f)
        (CategoryTheory.CategoryStruct.comp k g))
      h_1
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.twoBlockTriangular_det : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  (p : m → Prop) [inst_3 : DecidablePred p],
  (∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0) →
    M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_filter_containsKey_of_containsKey_eq_false_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValue? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.snd.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (F F_1 : Finset (α × α)) (e_F : F = F_1) {k : ℕ} (h : F.card = k) (b b_1 : α),
  b = b_1 →
    ∀ (i i_1 : Fin (k + 1)),
      i = i_1 → Finset.intervalGapsWithin.snd F h b i = Finset.intervalGapsWithin.snd F_1 ⋯ b_1 i_1
-- Init.Data.Option.Basic
/-- A case analysis function for `Option`.

Given a value for `none` and a function to apply to the contents of `some`, `Option.elim` checks
which constructor a given `Option` consists of, and uses the appropriate argument.

`Option.elim` is an elimination principle for `Option`. In particular, it is a non-dependent version
of `Option.recOn`. It can also be seen as a combination of `Option.map` and `Option.getD`.

Examples:
 * `(some "hello").elim 0 String.length = 5`
 * `none.elim 0 String.length = 0`
 -/
Option.elim : {α : Type u_1} → {β : Sort u_2} → Option α → β → (α → β) → β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Conditional expectation of a function, with notation `μ[f | m]`.

It is defined as 0 if any one of the following conditions is true:
- `m` is not a sub-σ-algebra of `m₀`,
- `μ` is not σ-finite with respect to `m`,
- `f` is not integrable. 

[Wikidata Q772232](https://www.wikidata.org/wiki/Q772232) -/
MeasureTheory.«term__[_|_]» : Lean.TrailingParserDescr
-- Init.Data.Option.Lemmas
Option.not_lt_pfilter : ∀ {α : Type u_1} [inst : LT α],
  (∀ (x : α), ¬x < x) → ∀ {o : Option α} {p : (a : α) → o = some a → Bool}, ¬o < o.pfilter p
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instSetLike : (G : Type u) → [inst : Group G] → [inst_1 : TopologicalSpace G] → SetLike (ClosedSubgroup G) G
-- Mathlib.CategoryTheory.Localization.Construction
/-- If `F₁` and `F₂` are functors `W.Localization ⥤ D`, a natural transformation `F₁ ⟶ F₂`
can be obtained from a natural transformation `W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂`.  -/
CategoryTheory.Localization.Construction.natTransExtension : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type uD} →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          {F₁ F₂ : CategoryTheory.Functor W.Localization D} → (W.Q.comp F₁ ⟶ W.Q.comp F₂) → (F₁ ⟶ F₂)