mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
Units.val_div_eq_div_val : ∀ {α : Type u} [inst : DivisionMonoid α] (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ / ↑u₂
-- Mathlib.Computability.ContextFreeGrammar
/-- The language (set of words) that can be generated by a given context-free grammar `g`.  -/
ContextFreeGrammar.language : {T : Type u_1} → ContextFreeGrammar T → Language T
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_union_of_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.Control.Fold
Monoid.foldlM.get : {m : Type u → Type u} → [inst : Monad m] → {α : Type u} → Monoid.foldlM m α → α → m α
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Ioi : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α) [inst_2 : Fintype ↑(Set.Ioi a)],
  Fintype.card ↑(Set.Ioi a) = (Finset.Ioi a).card
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.μ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Grp.forget₂Mon C) G H =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.Grp.forget₂Mon C).obj G)
        ((CategoryTheory.Grp.forget₂Mon C).obj H))
-- Mathlib.Topology.UniformSpace.Basic
/-- Entourages are neighborhoods of the diagonal.  -/
iSup_nhds_le_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], ⨆ x, nhds (x, x) ≤ uniformity α
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.descTruncGE_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n],
  ∃ f', f = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f'
-- Init.Data.Nat.Bitwise.Lemmas
Nat.mod_two_pow_shiftLeft_mod_two_pow : ∀ {a b c : ℕ}, (a % 2 ^ c) <<< b % 2 ^ c = a <<< b % 2 ^ c
-- Mathlib.RingTheory.FiniteType
/-- A commutative algebra is finitely generated if and only if it is a quotient
of a polynomial ring whose variables are indexed by a fintype.  -/
Algebra.FiniteType.iff_quotient_mvPolynomial' : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  Algebra.FiniteType R S ↔ ∃ ι x f, Function.Surjective ⇑f
-- Mathlib.RingTheory.Idempotents
completeOrthogonalIdempotents_iff : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} [inst_1 : Fintype I] (e : I → R),
  CompleteOrthogonalIdempotents e ↔ OrthogonalIdempotents e ∧ ∑ i, e i = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_add : ∀ {x y : ℝ},
  (((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨
      (∃ k, x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * Real.pi / 2) →
    Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_singleton.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] (a : α),
  SubMulAction.ofFixingSubgroup_of_singleton M a = { toFun := fun x => ⟨↑x, ⋯⟩, map_smul' := ⋯ }
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.castLE.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x x_1 : ℕ) → x ≤ x_1 → L.BoundedFormula α x → Sort u_4) →
      (x x_1 : ℕ) →
        (x_2 : x ≤ x_1) →
          (x_3 : L.BoundedFormula α x) →
            ((_m _n : ℕ) → (_h : _m ≤ _n) → motive _m _n _h FirstOrder.Language.BoundedFormula.falsum) →
              ((_m _n : ℕ) →
                  (h : _m ≤ _n) →
                    (t₁ t₂ : L.Term (α ⊕ Fin _m)) → motive _m _n h (FirstOrder.Language.BoundedFormula.equal t₁ t₂)) →
                ((_m _n : ℕ) →
                    (h : _m ≤ _n) →
                      (l : ℕ) →
                        (R : L.Relations l) →
                          (ts : Fin l → L.Term (α ⊕ Fin _m)) →
                            motive _m _n h (FirstOrder.Language.BoundedFormula.rel R ts)) →
                  ((_m _n : ℕ) → (h : _m ≤ _n) → (f₁ f₂ : L.BoundedFormula α _m) → motive _m _n h (f₁.imp f₂)) →
                    ((_m _n : ℕ) → (h : _m ≤ _n) → (f : L.BoundedFormula α (_m + 1)) → motive _m _n h f.all) →
                      motive x x_1 x_2 x_3
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The morphism of topological modules underlying a morphism in `TopRep k G`.  -/
TopRep.Hom.toTopModuleCatHom : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → {A B : TopRep k G} → A.Hom B → (TopModuleCat.of k ↑A ⟶ TopModuleCat.of k ↑B)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- For positive `x` and nonzero `y` and a Dirichlet character `χ` we have
`|L(χ^0, 1 + x)^3 * L(χ, 1 + x + I * y)^4 * L(χ^2, 1 + x + 2 * I * y)| ≥ 1`.  -/
DirichletCharacter.norm_LSeries_product_ge_one : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {x : ℝ},
  0 < x →
    ∀ (y : ℝ),
      ‖LSeries (fun n => 1 ↑n) (1 + ↑x) ^ 3 * LSeries (fun n => χ ↑n) (1 + ↑x + Complex.I * ↑y) ^ 4 *
            LSeries (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥
        1
-- Lean.Parser.Term
Lean.Parser.Term.matchExprElseAlt : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_inv : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x⁻¹.intDegree = -x.intDegree
-- Mathlib.Order.Hom.Basic
OrderIso.map_top : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α] [inst_3 : OrderTop β]
  (f : α ≃o β), f ⊤ = ⊤
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pullback_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.pullback (CategoryTheory.CategoryStruct.id X) R = R
-- Mathlib.Data.Fintype.Basic
/-- Induction principle to build a sequence, by adding one point at a time satisfying a given
relation with respect to all the previously chosen points.

More precisely, Assume that, for any finite set `s`, one can find another point satisfying
some relation `r` with respect to all the points in `s`. Then one may construct a
function `f : ℕ → α` such that `r (f m) (f n)` holds whenever `m < n`.
We also ensure that all constructed points satisfy a given predicate `P`.  -/
exists_seq_of_forall_finset_exists : ∀ {α : Type u_4} (P : α → Prop) (r : α → α → Prop),
  (∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) →
    ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
-- Init.System.IO
/-- Writes the provided string to the stream.
 -/
IO.FS.Stream.putStr : IO.FS.Stream → String → IO Unit
-- Mathlib.Algebra.Star.StarAlgHom
/-- Turn an element of a type `F` satisfying `NonUnitalAlgHomClass F R A B` and `StarHomClass F A B`
into an actual `NonUnitalStarAlgHom`. This is declared as the default coercion from `F` to
`A →⋆ₙₐ[R] B`.  -/
NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : DistribMulAction R A] →
              [inst_3 : Star A] →
                [inst_4 : NonUnitalNonAssocSemiring B] →
                  [inst_5 : DistribMulAction R B] →
                    [inst_6 : Star B] →
                      [inst_7 : FunLike F A B] → [NonUnitalAlgHomClass F R A B] → [StarHomClass F A B] → F → A →⋆ₙₐ[R] B
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.get!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β]
  (m : Std.DHashMap.Raw α fun x => β) (a : α),
  Std.DHashMap.Raw.Const.get! m a =
    if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.get! ⟨m, h⟩ a else default
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.coe_finsupp_sum : ∀ {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {γ : Type u_9} [inst_6 : Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂),
  ⇑(t.sum g) = ⇑(t.sum fun i d => g i d)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.limitCLM_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} {V : Type u_6} [inst_6 : AddCommGroup V]
  [inst_7 : Module ℝ V] [t : TopologicalSpace V] [inst_8 : IsTopologicalAddGroup V] [inst_9 : ContinuousSMul ℝ V]
  [inst_10 : LocallyConvexSpace ℝ V] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F] [inst_13 : Module 𝕜 V]
  [inst_14 : IsScalarTower ℝ 𝕜 V] (toFun : TestFunction Ω F n → V)
  (T : (K : TopologicalSpace.Compacts E) → ↑K ⊆ ↑Ω → ContDiffMapSupportedIn E F n K →L[𝕜] V)
  (toFun_eq_T :
    ∀ (K : TopologicalSpace.Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K),
      toFun (TestFunction.ofSupportedIn K_sub_Ω f) = (T K K_sub_Ω) f)
  (a : TestFunction Ω F n), (TestFunction.limitCLM 𝕜 toFun T toFun_eq_T) a = toFun a
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiff_of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞}
  [Subsingleton F], ContDiff 𝕜 n f
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.van_kampen' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Adhesive C] [CategoryTheory.Mono g] (H : CategoryTheory.IsPushout f g h i), H.IsVanKampen
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.single_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {a : α} {b : β}, (RBTree.RBMap.single a b).toList = [(a, b)]
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)
-- Mathlib.RingTheory.Norm.Transitivity
/-- For `L/K` a finite separable extension of fields and `E` an algebraically closed extension
of `K`, the norm (down to `K`) of an element `x` of `L` is equal to the product of the images
of `x` over all the `K`-embeddings `σ` of `L` into `E`.  -/
Algebra.norm_eq_prod_embeddings : ∀ {L : Type u_6} (K : Type u_7) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : Type u_9)
  [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : FiniteDimensional K L] [Algebra.IsSeparable K L] [IsAlgClosed E]
  (x : L), (algebraMap K E) ((Algebra.norm K) x) = ∏ σ, σ x
-- Std.Data.DTreeMap.Internal.Model
/-- Needle was larger than key at this node: return key-value pair and unexplored left subtree,
recursion will continue in right subtree.  -/
Std.DTreeMap.Internal.Impl.ExplorationStep.gt : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {k : α → Ordering} →
        List ((a : α) × β a) → (a : α) → k a = Ordering.gt → β a → Std.DTreeMap.Internal.Impl.ExplorationStep α β k
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instDivSubtypeMemAddSubgroup : {R : Type u_1} → [inst : Field R] → [inst_1 : StarRing R] → Div ↥(selfAdjoint R)
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isQuasiInverse_subtype_projectionOnto : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} [IsNoetherian K ↥T] (hST : IsCompl S T), S.subtype.IsQuasiInverse (S.projectionOnto T hST)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_inv_app_comp_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).inv.app T))
      (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) =
    CategoryTheory.Limits.pullback.fst T.hom g
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_bot : ∀ (A : Type u_2) (B : Type u_3) [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : Algebra A B] [FaithfulSMul A B],
  Ideal.under A ⊥ = ⊥
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_isCoprime_of_dvd_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime y z → x ∣ y → IsCoprime x z
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cosh_add_pi_mul_I : ∀ (z : ℂ), Complex.cosh (z + ↑Real.pi * Complex.I) = -Complex.cosh z
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `(a,b)` is the kernel pair of `f`, and `f` is a regular epimorphism, then
`f` is a coequalizer morphism of `a` and `b`.
 -/
CategoryTheory.IsKernelPair.toCoequalizer' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R X Y : C} →
      {f : X ⟶ Y} →
        {a b : R ⟶ X} →
          (k : CategoryTheory.IsKernelPair f a b) →
            [CategoryTheory.IsRegularEpi f] → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteLimits F] (X : C),
  CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (F.toRightDerivedZero.app X) =
    CategoryTheory.CategoryStruct.id ((F.rightDerived 0).obj X)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- `f` is an epi if the pushout cocone `(𝟙 X, 𝟙 X)` is a colimit for the pair `(f, f)`.
The converse is given in `PushoutCocone.isColimitMkIdId`.
 -/
CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  (t :
    CategoryTheory.Limits.IsColimit
      (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)
        ⋯)),
  CategoryTheory.Epi f
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.rel.id : ∀ {I : Type u} [inst : DecidableEq I] {R : Type v} [inst_1 : CommSemiring R] {A : I → Type w}
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {i : I},
  LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.singletonFinsubgraph.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (v : V), SimpleGraph.singletonFinsubgraph v = ⟨G.singletonSubgraph v, ⋯⟩
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.toContinuousLinearMap.eq_1 : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M₁ M₂) [inst_7 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι),
  f.toContinuousLinearMap m i = { toLinearMap := f.toLinearMap m i, cont := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Cache decision variables used when splitting on disequalities.
This is necessary because the same disequality may be in different conflicts.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.diseqSplits : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PHashMap Lean.Grind.Linarith.Poly Lean.FVarId
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.ofFinEmb_surjective : ∀ (n : ℕ) (β : Type u_2), Function.Surjective (Set.powersetCard.ofFinEmb n β)
-- Lean.Environment
Lean.ImportM.Context.mk.sizeOf_spec : ∀ (env : Lean.Environment) (opts : Lean.Options), sizeOf { env := env, opts := opts } = 1 + sizeOf env + sizeOf opts
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV2.mk.sizeOf_spec : ∀ (toTZifV1 : Std.Time.TimeZone.TZif.TZifV1) (footer : Option String),
  sizeOf { toTZifV1 := toTZifV1, footer := footer } = 1 + sizeOf toTZifV1 + sizeOf footer
-- Init.Data.BitVec.Lemmas
BitVec.le_of_lt : ∀ {w : ℕ} {x y : BitVec w}, x < y → x ≤ y
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.topologicalClosure_minimal : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A] {s t : StarSubalgebra R A},
  s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Std.Data.TreeSet.Basic
/-- Retrieves the key from the set that matches `a`. Ensures that such a key exists by requiring a proof
of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the set.
 -/
Std.TreeSet.get : {α : Type u} → {cmp : α → α → Ordering} → (t : Std.TreeSet α cmp) → (a : α) → a ∈ t → α
-- Mathlib.Algebra.Module.LinearMap.End
RingEquiv.moduleEndSelfOp_apply : ∀ (R : Type u_1) [inst : Semiring R] (s : R), (RingEquiv.moduleEndSelfOp R) s = DistribSMul.toLinearMap Rᵐᵒᵖ R s
-- Lean.Parser.Types
Lean.Parser.InputContext.fileMap : Lean.Parser.InputContext → Lean.FileMap
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isDetector_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsDetector G ↔
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulBackwardPatternModel.skipSuffix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice},
  String.Slice.Pattern.BackwardPattern.skipSuffix? pat s = none ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat s.endPos
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.coxeterWeightIn_ne_four : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  {i j : ι} [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [P.IsReduced],
  i ≠ j → P.root i ≠ -P.root j → P.coxeterWeightIn S i j ≠ 4
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk_eq_top : ∀ {M : Type u_1} [inst : MulOneClass M] (toSubsemigroup : Subsemigroup M) (one_mem' : 1 ∈ toSubsemigroup.carrier),
  { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊤ ↔ toSubsemigroup = ⊤
-- Batteries.Data.DList.Lemmas
_private.Batteries.Data.DList.Lemmas.0.Batteries.DList.toList.match_1.eq_1 : ∀ {α : Type u_1} (motive : Batteries.DList α → Sort u_2) (f : List α → List α)
  (invariant : ∀ (l : List α), f l = f [] ++ l)
  (h_1 :
    (f : List α → List α) →
      (invariant : ∀ (l : List α), f l = f [] ++ l) → motive { apply := f, invariant := invariant }),
  (match { apply := f, invariant := invariant } with
    | { apply := f, invariant := invariant } => h_1 f invariant) =
    h_1 f invariant
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.mk : ∀ {G : Type u_1} [inst : Group G], Nat.card G = 4 → Monoid.exponent G = 2 → IsKleinFour G
-- Mathlib.Probability.Kernel.Disintegration.Basic
/-- A kernel `ρCond` is a conditional kernel for a measure `ρ` if it disintegrates it in the sense
that `ρ.fst ⊗ₘ ρCond = ρ`.  -/
MeasureTheory.Measure.IsCondKernel : {α : Type u_1} →
  {Ω : Type u_3} →
    {mα : MeasurableSpace α} →
      {mΩ : MeasurableSpace Ω} → MeasureTheory.Measure (α × Ω) → ProbabilityTheory.Kernel α Ω → Prop
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ioc' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ioc a b ↔ x ≤ b ∧ a < x
-- Init.Data.Sum.Lemmas
Sum.lex_acc_inl : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {β : Type u_2} {s : β → β → Prop}, Acc r a → Acc (Sum.Lex r s) (Sum.inl a)
-- Init.Control.StateRef
instMonadControlStateRefT' : (ω σ : Type) → (m : Type → Type) → MonadControl m (StateRefT' ω σ m)
-- Mathlib.Topology.Order.LeftRightNhds
nhdsLT_eq_bot_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  nhdsWithin a (Set.Iio a) = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X))
      ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X)
-- Mathlib.RingTheory.Ideal.IsPrincipal
/-- The `MulEquiv` version of `Ideal.associatesEquivIsPrincipal`.  -/
Ideal.associatesMulEquivIsPrincipal : (R : Type u_1) → [inst : CommRing R] → [IsDomain R] → Associates R ≃* ↥(Ideal.isPrincipalSubmonoid R)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ord.eq_1 : ∀ (I : Type u) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (i : I),
  Profinite.NobelingProof.ord I i = (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_compl : ∀ {α : Type u_1} {s t : Set α}, s \ tᶜ = s ∩ t
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- Metric space structure on `Stream' α` considering `α` as a discrete metric space.  -/
Tactic.ComputeAsymptotics.Seq.instMetricSpaceStream' : {α : Type u_1} → MetricSpace (Stream' α)
-- Mathlib.ModelTheory.Bundled
/-- Shrinks a small model to a particular universe.  -/
FirstOrder.Language.Theory.ModelType.shrink : {L : FirstOrder.Language} → {T : L.Theory} → (M : T.ModelType) → [Small.{w', w} ↑M] → T.ModelType
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticAt.im_ofReal : ∀ {f : ℂ → ℂ} {x : ℝ}, AnalyticAt ℂ f ↑x → AnalyticAt ℝ (fun x => (f ↑x).im) x
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_eq_nil : ∀ {m n : ℕ}, n ≤ m → (m<...=n).toArray = #[]
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.isEmpty = true → t.getD a fallback = fallback
-- Lean.Server.InfoUtils
Lean.Elab.Info.isCompletion : Lean.Elab.Info → Bool