mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Complex.Basic
Complex.div_ofReal_im : ∀ (z : ℂ) (x : ℝ), (z / ↑x).im = z.im / x
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.preprocessExprPattern : Lean.Expr → List Lean.Name → optParam Bool false → Lean.MetaM (List Lean.Name × Lean.Expr)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsFiniteKernelSectLOfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (b : β) [ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.IsFiniteKernel (κ.sectL b)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont.mk.inj : ∀ {resultType : Lean.Expr} {k : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr} {resultType_1 : Lean.Expr}
  {k_1 : Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr},
  { resultType := resultType, k := k } = { resultType := resultType_1, k := k_1 } → resultType = resultType_1 ∧ k = k_1
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.le_smul_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), ∃ n, s ≤ n • s.dedup
-- Mathlib.Data.Finsupp.MonomialOrder
/-- `syn` is a linearly ordered cancellative additive commutative monoid  -/
MonomialOrder.isOrderedAddMonoid_syn : ∀ {σ : Type u_1} (self : MonomialOrder σ), IsOrderedAddMonoid self.syn
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.IsArgminEstimator.property : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Θ]
  [inst_1 : Nonempty Θ] {𝓨 : Type u_4} [inst_2 : MeasurableSpace 𝓨] {ℓ : Θ → 𝓨 → ENNReal}
  {P : ProbabilityTheory.Kernel Θ 𝓧} [inst_3 : ProbabilityTheory.IsFiniteKernel P] {π : MeasureTheory.Measure Θ}
  [inst_4 : MeasureTheory.IsFiniteMeasure π] {f : 𝓧 → 𝓨},
  ProbabilityTheory.IsArgminEstimator ℓ P π f →
    ∀ᵐ (x : 𝓧) ∂π.bind ⇑P,
      ∫⁻ (θ : Θ), ℓ θ (f x) ∂(ProbabilityTheory.posterior P π) x =
        ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∈ m₂ → Std.ExtDHashMap.Const.getD (m₁ ∩ m₂) k fallback = Std.ExtDHashMap.Const.getD m₁ k fallback
-- Lean.Environment
Lean.Environment.isImportedConst : Lean.Environment → Lean.Name → Bool
-- Std.Data.HashMap.Lemmas
Std.HashMap.union_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β}, m₁.union m₂ = m₁ ∪ m₂
-- Lean.Structure
Lean.StructureResolutionState.mk : Lean.PHashMap Lean.Name (Array Lean.Name) → Lean.StructureResolutionState
-- Mathlib.Tactic.NormNum.Core
_private.Mathlib.Tactic.NormNum.Core.0.Mathlib.Meta.NormNum.mkNormNumExt.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) →
                  motive ⟨Std.IterStep.yield it' out, property⟩) →
            ((it' : Std.Iter β) →
                (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩) →
              ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Shortcut instance, saving 8.5% of compilation time in
`Mathlib/Analysis/InnerProductSpace/Adjoint.lean`.

(This instance was pinpointed by benchmarks; we didn't do an in depth investigation why it is
specifically needed.)
 -/
LinearIsometryEquiv.instCoeFun : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun x => E → E₂
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.instInhabitedExpr.default : Nat.Internal.SOM.Expr
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instContMDiffInv₀OfSomeENatTopOfLEInfty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {a : WithTop ℕ∞}
  [ContMDiffInv₀ I (↑⊤) G] [h : ENat.LEInfty a], ContMDiffInv₀ I a G
-- Aesop.Forward.PremiseIndex
Aesop.PremiseIndex.mk : ℕ → Aesop.PremiseIndex
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.sum_affineCombinationLineMapWeights : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_4} (s : Finset ι) [inst_1 : DecidableEq ι] {i j : ι},
  i ∈ s → j ∈ s → ∀ (c : k), ∑ t ∈ s, Finset.affineCombinationLineMapWeights i j c t = 1
-- Lean.Meta.Match.NamedPatterns
Lean.Meta.Match.isNamedPattern : Lean.Expr → Bool
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.OfKernel.instRKHS : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              {K : Matrix X X (V →L[𝕜] V)} → [inst_4 : Fact K.PosSemidef] → RKHS 𝕜 (RKHS.OfKernel K) X V
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < b → b ∣ a → (a / b < c ↔ a < b * c)
-- Mathlib.LinearAlgebra.Basis.Cardinality
_private.Mathlib.LinearAlgebra.Basis.Cardinality.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_eq_append : ∀ {m n : ℤ}, m ≤ n → (m...=n).toList = (m...n).toList ++ [n]
-- Std.Http.Protocol.H1.Event
/-- Indicates that a response is required.
 -/
Std.Http.Protocol.H1.Event.needAnswer : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseLit : Std.Internal.Parsec.ByteArray.Parser ℤ
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.MakeEditLinkProps : Type
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.dimension_ofAlgEquiv : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {T : Type u_1} [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  (P.ofAlgEquiv e).dimension = P.dimension
-- Lean.Data.Lsp.Utf16
Lean.FileMap.leanPosToLspPos : Lean.FileMap → Lean.Position → Lean.Lsp.Position
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smulMemClass : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SMulMemClass (Submodule R M) R M
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).e =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f))
      (CategoryTheory.Abelian.coimageImageComparison f)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.symm_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  {f₀ f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (x : ↑unitInterval × X), F.symm x = F (unitInterval.symm x.1, x.2)
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsSatisfiable.isFinitelySatisfiable : ∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsSatisfiable → T.IsFinitelySatisfiable
-- Init.Data.Ord.BitVec
BitVec.instLawfulEqOrd : ∀ {n : ℕ}, Std.LawfulEqOrd (BitVec n)
-- Mathlib.Algebra.Lie.Basic
LieHom.instInhabited : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → Inhabited (L₁ →ₗ⁅R⁆ L₂)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  {f : (a : α) → β a → γ a},
  m.WF → (Std.DHashMap.Raw.map f m).toList.Perm (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) m.toList)
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.HasIdealSupport.smul_mem_support : ∀ {R : Type u_1} {inst : CommRing R} (P : RingPreordering R) [self : P.HasIdealSupport] (x : R) {a : R},
  a ∈ P.supportAddSubgroup → x * a ∈ P.supportAddSubgroup
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1_is_congruence : ∀ (N : ℕ) [NeZero N], CongruenceSubgroup.IsCongruenceSubgroup (CongruenceSubgroup.Gamma1 N)
-- Std.Data.HashMap.Basic
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.HashMap.emptyWithCapacity : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.HashMap α β
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- Every element of `α` is eventually a member of `s` along `atTop` on `Finset α`.  -/
Filter.eventually_finset_mem_atTop : ∀ {α : Type u_3} (i : α), ∀ᶠ (s : Finset α) in Filter.atTop, i ∈ s
-- Mathlib.Data.Set.Image
Set.forall_subtype_range_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : ↑(Set.range f) → Prop},
  (∀ (a : ↑(Set.range f)), p a) ↔ ∀ (i : ι), p ⟨f i, ⋯⟩
-- Init.Data.BitVec.Lemmas
/-- Prove nonequality of bitvectors in terms of nat operations.  -/
BitVec.toNat_ne_iff_ne : ∀ {n : ℕ} {x y : BitVec n}, x.toNat ≠ y.toNat ↔ x ≠ y
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- The functor `F.mapTriangle` commutes with the shift.  -/
CategoryTheory.Functor.mapTriangleCommShiftIso : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                [inst_5 : CategoryTheory.Preadditive C] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [F.Additive] →
                      (n : ℤ) →
                        (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).comp F.mapTriangle ≅
                          F.mapTriangle.comp (CategoryTheory.Pretriangulated.Triangle.shiftFunctor D n)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage.eq_1 : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal),
  MeasureTheory.laverage μ f = ∫⁻ (x : α), f x ∂(μ Set.univ)⁻¹ • μ
-- Mathlib.Topology.Order.Compact
cocompact_eq_atBot_atTop : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMaxOrder α] [NoMinOrder α]
  [OrderClosedTopology α] [CompactIccSpace α], Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.cons.inj : ∀ {V : Type u} {inst : Quiver V} {a b c : V} {a_1 : Quiver.Path a b} {a_2 : b ⟶ c} {b_1 : V} {a_3 : Quiver.Path a b_1}
  {a_4 : b_1 ⟶ c}, a_1.cons a_2 = a_3.cons a_4 → b = b_1 ∧ a_1 ≍ a_3 ∧ a_2 ≍ a_4
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.edistLtTopSetoid`.

---

Relation “two points are at a finite edistance” is an equivalence relation.  -/
EMetric.edistLtTopSetoid : {α : Type u} → [PseudoEMetricSpace α] → Setoid α
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.eventually_isCompact_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α),
  ∀ᶠ (r : ℝ) in nhds 0, IsCompact (Metric.closedBall x r)
-- Mathlib.Algebra.Lie.Matrix
Matrix.reindexLieEquiv_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {m : Type w₁}
  [inst_3 : DecidableEq m] [inst_4 : Fintype m] (e : n ≃ m) (M : Matrix n n R),
  (Matrix.reindexLieEquiv e) M = (Matrix.reindex e e) M
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓObjEquivHom_naturality_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type w)] [inst_2 : CategoryTheory.HasGlobalSectionsFunctor J (Type w)]
  {X : Type w} [inst_3 : Unique X] {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G)
  (x : (CategoryTheory.constantSheaf J (Type w)).obj X ⟶ F),
  (CategoryTheory.Sheaf.ΓObjEquivHom J G X).symm (CategoryTheory.CategoryStruct.comp x f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Sheaf.Γ J (Type w)).map f))
      ((CategoryTheory.Sheaf.ΓObjEquivHom J F X).symm x)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_surjective : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α}, Function.Surjective (Set.projIic b)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionIdentifier : Hashable Lean.Lsp.CompletionIdentifier
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.add_slash : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {inst : Monoid G} {inst_1 : AddMonoid α} [self : SlashAction β G α]
  (k : β) (g : G) (a b : α), SlashAction.map k g (a + b) = SlashAction.map k g a + SlashAction.map k g b
-- Mathlib.Tactic.Linarith.Datatypes
/-- Defines a lex ordering on `Linexp`. This function is performance critical.
 -/
Mathlib.Tactic.Linarith.Linexp.cmp : Mathlib.Tactic.Linarith.Linexp → Mathlib.Tactic.Linarith.Linexp → Ordering
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) QuasiErgodic._auto_1},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ μ → PreErgodic f μ → QuasiErgodic f μ
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
`n`, equipped with Haar measure, and let `1 < p < n` and `0 < q ≤ (p⁻¹ - (finrank ℝ E : ℝ)⁻¹)⁻¹`.
Then the `L^q` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
the Fréchet derivative of `u`.

Note: The codomain of `u` needs to be a finite-dimensional normed space.
 -/
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_le : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_4} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F] {u : E → F} {s : Set E},
  ContDiff ℝ 1 u →
    Function.support u ⊆ s →
      ∀ {p q : NNReal},
        1 ≤ p →
          p < ↑(Module.finrank ℝ E) →
            ↑p⁻¹ - (↑(Module.finrank ℝ E))⁻¹ ≤ (↑q)⁻¹ →
              Bornology.IsBounded s →
                MeasureTheory.eLpNorm u (↑q) μ ≤
                  ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.resolvent_isBigO_inv : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), resolvent a =O[Bornology.cobounded 𝕜] Inv.inv
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_le_one_of_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], a ≤ 1 → ⌊a⌋₊ ≤ 1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_tProd_elim : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (i : δ) → MeasurableSpace (X i)] [inst_1 : DecidableEq δ] {l : List δ}
  {i : δ} (hi : i ∈ l), Measurable fun v => v.elim hi
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.whnfCore.go : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.ext : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {f f' : M [⋀^ι]→ₗ[R] N},
  (∀ (x : ι → M), f x = f' x) → f = f'
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.diam_preimage : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (h : α ≃ᵢ β) (s : Set β),
  Metric.diam (⇑h ⁻¹' s) = Metric.diam s
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.down_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C}
  (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y)
  (g : CategoryTheory.WithInitial.of Y ⟶ CategoryTheory.WithInitial.of Z),
  CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.down f) (CategoryTheory.WithInitial.down g)
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rci_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs lo...xs.size
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instAdditiveArrowRightFunctor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V], (CategoryTheory.Preadditive.RightFreyd.rightFunctor V).Additive
-- Lean.CoreM
Lean.Core.Context.mk.sizeOf_spec : ∀ (fileName : String) (fileMap : Lean.FileMap) (options : Lean.Options) (currRecDepth maxRecDepth : ℕ)
  (ref : Lean.Syntax) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (initHeartbeats maxHeartbeats : ℕ)
  (quotContext : Lean.Name) (currMacroScope : Lean.MacroScope) (diag : Bool) (cancelTk? : Option IO.CancelToken)
  (suppressElabErrors : Bool) (inheritedTraceOptions : Std.HashSet Lean.Name),
  sizeOf
      { fileName := fileName, fileMap := fileMap, options := options, currRecDepth := currRecDepth,
        maxRecDepth := maxRecDepth, ref := ref, currNamespace := currNamespace, openDecls := openDecls,
        initHeartbeats := initHeartbeats, maxHeartbeats := maxHeartbeats, quotContext := quotContext,
        currMacroScope := currMacroScope, diag := diag, cancelTk? := cancelTk?,
        suppressElabErrors := suppressElabErrors, inheritedTraceOptions := inheritedTraceOptions } =
    1 + sizeOf fileName + sizeOf fileMap + sizeOf options + sizeOf currRecDepth + sizeOf maxRecDepth + sizeOf ref +
                        sizeOf currNamespace +
                      sizeOf openDecls +
                    sizeOf initHeartbeats +
                  sizeOf maxHeartbeats +
                sizeOf quotContext +
              sizeOf currMacroScope +
            sizeOf diag +
          sizeOf cancelTk? +
        sizeOf suppressElabErrors +
      sizeOf inheritedTraceOptions
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
ModularForm.toCuspForm_apply : ∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
  (h : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) (z : UpperHalfPlane), (f.toCuspForm h) z = f z
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_finite : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [Finite ι] {F : ι → β → α}
  {S : Set β}, UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.instIsWellOrderContinuousFin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (F : CategoryTheory.Functor (Fin n) C),
  F.IsWellOrderContinuous
-- Mathlib.RingTheory.WittVector.StructurePolynomial
/-- `wittPolynomial p R n` is the `n`-th Witt polynomial
with respect to a prime `p` with coefficients in a commutative ring `R`.
It is defined as:

`∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`.  -/
Witt.termW__1 : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine_mul_k : ℤ → ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Data.Finset.Defs
Finset.mk.inj : ∀ {α : Type u_4} {val : Multiset α} {nodup : val.Nodup} {val_1 : Multiset α} {nodup_1 : val_1.Nodup},
  { val := val, nodup := nodup } = { val := val_1, nodup := nodup_1 } → val = val_1
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.mk : {α : Type u_4} →
  [toGeneralizedCoheytingAlgebra : GeneralizedCoheytingAlgebra α] →
    [toOrderTop : OrderTop α] → [toHNot : HNot α] → (∀ (a : α), ⊤ \ a = ￢a) → CoheytingAlgebra α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Any localization of a cancellative commutative additive monoid is cancellative.  -/
AddSubmonoid.LocalizationMap.addCancelCommMonoid : {M : Type u_3} →
  {N : Type u_4} →
    [inst : AddCancelCommMonoid M] →
      {S : AddSubmonoid M} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → AddCancelCommMonoid N
-- Std.Http.Data.URI.Encoding
/-- Converts an `EncodedQueryString` to a `String`, given a proof that all characters satisfying `r` are ASCII.
 -/
Std.Http.URI.EncodedQueryString.toString : {r : UInt8 → Bool} → Std.Http.URI.EncodedQueryString r → String
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?_add : ∀ {α : Type u} (s : Stream'.WSeq α) (m n : ℕ), s.get? (m + n) = (s.drop m).get? n
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whisker a 1-morphism to a lift.
```
                    b
                  ◹ |
           lift /   |      | counit
              /     | f    ▽
            /       ▽
x - - - ▷ c - - - ▷ a
     h         g
```
 -/
CategoryTheory.Bicategory.RightLift.whisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          CategoryTheory.Bicategory.RightLift f g →
            {x : B} → (h : x ⟶ c) → CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp h g)
-- Aesop.Tree.State
_private.Aesop.Tree.State.0.Aesop.markUnprovableCore : Aesop.TreeRef → BaseIO Unit
-- Mathlib.Tactic.Order.ToInt
_private.Mathlib.Tactic.Order.ToInt.0.Mathlib.Tactic.Order.ToInt.toInt.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (k : Fin n),
  Mathlib.Tactic.Order.ToInt.toInt val k = ⋯.choose k
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.rfl.sizeOf_spec : ∀ (done : optParam Bool false), sizeOf (Lean.Meta.Sym.DSimp.Result.rfl done) = 1 + sizeOf done
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.const.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  {value value_1 : BaseType e},
  Mathlib.Tactic.Ring.Common.ExProd.const value = Mathlib.Tactic.Ring.Common.ExProd.const value_1 → value = value_1