mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.of_hasBinaryProduct' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X Y : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] [inst_2 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
    (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.instCoe : {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} → Coe (M [⋀^ι]→ₗ[R] N) (MultilinearMap R (fun x => M) N)
-- Mathlib.Order.Lattice
inf_assoc : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div : ∀ (a : UnitAddCircle), DifferentiableAt ℂ (fun s => HurwitzZeta.hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P P_1 : RootPairing ι R M N) (e_P : P = P_1)
  (S : Type u_6) [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : P.IsValuedIn S] (i i_1 : ι),
  i = i_1 → ∀ (j j_1 : ι), j = j_1 → P.pairingIn S i j = P_1.pairingIn S i_1 j_1
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.monoidalClosed_closed_adj : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Functor D C),
  CategoryTheory.Closed.adj =
    { unit := X.closedUnit, counit := X.closedCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_mul_prod_of_opNorm_le_of_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] {f : E [⋀^ι]→L[𝕜] F} {m : ι → E} {C : ℝ} {b : ι → ℝ},
  ‖f‖ ≤ C → (∀ (i : ι), ‖m i‖ ≤ b i) → ‖f m‖ ≤ C * ∏ i, b i
-- Mathlib.Data.Set.List
_private.Mathlib.Data.Set.List.0.Option.getD.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (opt : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive opt
-- Batteries.Data.List.Lemmas
List.dropPrefix?.eq_def : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : List α),
  x.dropPrefix? x_1 =
    match x, x_1 with
    | list, [] => some list
    | [], head :: tail => none
    | a :: as, b :: bs => if (a == b) = true then as.dropPrefix? bs else none
-- Mathlib.Topology.Sheaves.Functors
/-- The pushforward functor.
 -/
TopCat.Sheaf.pushforward : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} → (X ⟶ Y) → CategoryTheory.Functor (TopCat.Sheaf C X) (TopCat.Sheaf C Y)
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- `∀ᵐ a ∂μ, p a` means that `p a` for a.e. `a`, i.e. `p` holds true away from a null set.

This is notation for `Filter.Eventually p (MeasureTheory.ae μ)`.  -/
MeasureTheory.«term∀ᵐ_∂_,_» : Lean.ParserDescr
-- Lean.Elab.App
/-- Save information for producing error messages.  -/
Lean.Elab.Term.ElabElim.saveArgInfo : Lean.Expr → Lean.Name → Lean.Elab.Term.ElabElim.M Unit
-- Mathlib.NumberTheory.PythagoreanTriples
/-- A triple is still a triple if you multiply `x`, `y` and `z`
by a constant `k`.  -/
PythagoreanTriple.mul : ∀ {x y z : ℤ}, PythagoreanTriple x y z → ∀ (k : ℤ), PythagoreanTriple (k * x) (k * y) (k * z)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.filter f t).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ t), f (t.get k h) = true
-- Mathlib.Analysis.Convex.Segment
midpoint_mem_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Invertible 2] (x y : E), midpoint 𝕜 x y ∈ openSegment 𝕜 x y
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.w : ∀ {X Y : SSet} (i : X ⟶ Y) (d : ℕ),
  CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.t i d) (SSet.relativeCellComplexOfMono.r i d) =
    CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.l i d) (SSet.relativeCellComplexOfMono.b i d)
-- Init.Data.Array.Monadic
Array.filterMapM_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {as bs : Array α},
  as = bs → ∀ {f g : α → m (Option β)}, (∀ (a : α), f a = g a) → Array.filterMapM f as = Array.filterMapM g bs
-- Lean.Parser.Term
Lean.Parser.Termination.coinductiveFixpoint.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Hom.ContinuousEval
/-- A typeclass saying that `F` is a bundled morphism class (in the sense of `FunLike`)
with a topology such that `fun (f, x) : F × X ↦ f x` is a continuous function.  -/
ContinuousEval : (F : Type u_1) →
  (X : outParam (Type u_2)) →
    (Y : outParam (Type u_3)) →
      [FunLike F X Y] → [TopologicalSpace F] → [TopologicalSpace X] → [TopologicalSpace Y] → Prop
-- Mathlib.Tactic.MinImports
/-- Extracts the names of the declarations in `env` on which `decl` depends.  -/
Mathlib.Command.MinImports.getVisited : Lean.Name → Lean.Elab.Command.CommandElabM Lean.NameSet
-- Mathlib.Order.ModularLattice
IsUpperModularLattice.to_isWeakUpperModularLattice : ∀ {α : Type u_1} [inst : Lattice α] [IsUpperModularLattice α], IsWeakUpperModularLattice α
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_trans : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2}
  [inst_5 : Ring U] [inst_6 : Algebra R U] (h'' : IsAdjoinRoot U f),
  (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.one_le_dist_inl_inr : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {x : X} {y : Y},
  1 ≤ Metric.Sum.dist (Sum.inl x) (Sum.inr y)
-- Mathlib.Order.WithBot
WithTop.lt_untopD_iff : ∀ {α : Type u_1} {a b : α} [inst : LT α] {x : WithTop α}, (x = ⊤ → b < a) → (b < WithTop.untopD a x ↔ ↑b < x)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Transfer `CompleteAtomicBooleanAlgebra` across an `Equiv`.  -/
Equiv.completeAtomicBooleanAlgebra : {α : Type u} → {β : Type v} → α ≃ β → [CompleteAtomicBooleanAlgebra β] → CompleteAtomicBooleanAlgebra α
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are open embeddings, and `S ⟶ T`
is mono, then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an open embedding.

```
W ⟶ Y
 ↘   ↘
  S ⟶ T
 ↗   ↗
X ⟶ Z
```
 -/
TopCat.pullback_map_isOpenEmbedding : ∀ {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁) →
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂) →
      ∀ (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃]
        (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
        (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂),
        Topology.IsOpenEmbedding
          ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasStrictDerivAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, x ≠ 0 → HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x
-- Mathlib.Order.Filter.CountablyGenerated
Filter.Sup.isCountablyGenerated : ∀ {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated], (f ⊔ g).IsCountablyGenerated
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.utf8DecodeChar?_eq_assemble₃ : ∀ {b : ByteArray} (hb : 3 ≤ b.size),
  ByteArray.utf8DecodeChar?.parseFirstByte b[0] = ByteArray.utf8DecodeChar?.FirstByte.twoMore →
    b.utf8DecodeChar? 0 = ByteArray.utf8DecodeChar?.assemble₃ b[0] b[1] b[2]
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.invRev_length : ∀ {α : Type u} {L₁ : List (α × Bool)}, (FreeGroup.invRev L₁).length = L₁.length
-- Init.MethodSpecsSimp
XorOp.xor_hXor : ∀ {α : Type u_1} [inst : XorOp α], XorOp.xor = HXor.hXor
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.instHasFiniteBiproducts : CategoryTheory.Limits.HasFiniteBiproducts AddCommGrpCat
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap φ =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.hom (CategoryTheory.CategoryStruct.comp γ.φH h₂.homologyIso.inv)
-- Mathlib.Data.String.Basic
/-- `<` on string iterators. This coincides with `<` on strings as lists.  -/
String.ltb : String.Legacy.Iterator → String.Legacy.Iterator → Bool
-- Mathlib.Logic.Equiv.PartialEquiv
/-- `EqOnSource e e'` means that `e` and `e'` have the same source, and coincide there. Then `e`
and `e'` should really be considered the same partial equiv.  -/
PartialEquiv.EqOnSource : {α : Type u_1} → {β : Type u_2} → PartialEquiv α β → PartialEquiv α β → Prop
-- Mathlib.Data.Nat.Bits
Nat.bits_append_bit : ∀ (n : ℕ) (b : Bool), (n = 0 → b = true) → (Nat.bit b n).bits = b :: n.bits
-- Std.Do.PredTrans
/-- Adds the ability to make assertions about early termination to a predicate transformer with
postcondition shape `ps`, resulting in postcondition shape `.except PUnit ps`. This is done by
interpreting `OptionT (PredTrans ps) α` into `PredTrans (.except PUnit ps) α`, which models the type
`Option` as being equivalent to `Except PUnit`.
 -/
Std.Do.PredTrans.pushOption : {ps : Std.Do.PostShape} →
  {α : Type u_1} → OptionT (Std.Do.PredTrans ps) α → Std.Do.PredTrans (Std.Do.PostShape.except PUnit.{u_1 + 1} ps) α
-- Std.Data.String.ToInt
String.Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- `ModuleCat.Hom.hom` bundled as a linear equivalence.  -/
ModuleCat.homLinearEquiv : {R : Type u} →
  [inst : Ring R] →
    {M N : ModuleCat R} →
      {S : Type u_1} →
        [inst_1 : Semiring S] → [inst_2 : Module S ↑N] → [inst_3 : SMulCommClass R S ↑N] → (M ⟶ N) ≃ₗ[S] ↑M →ₗ[R] ↑N
-- Mathlib.Order.InitialSeg
PrincipalSeg.acc : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans β s] (f : PrincipalSeg r s) (a : α),
  Acc r a ↔ Acc s (f.toRelEmbedding a)
-- Mathlib.Algebra.GCDMonoid.Basic
Associated.eq_of_normalized : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α},
  Associated a b → normalize a = a → normalize b = b → a = b
-- Batteries.Data.FloatArray
/-- `mapM f a` applies the monadic function `f` to each element of the array.  -/
FloatArray.mapM : {m : Type → Type u_1} → [Monad m] → FloatArray → (Float → m Float) → m FloatArray
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_inclusion : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K') (x : ↥K), ↑((LieSubalgebra.inclusion h) x) = ↑x
-- Std.Http.Data.Headers
/-- Converts the headers to a list of key-value pairs (flattened). Each header with multiple values produces
multiple pairs.
 -/
Std.Http.Headers.toList : Std.Http.Headers → List (Std.Http.Header.Name × Std.Http.Header.Value)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.instSymmParallel : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P], Std.Symm AffineSubspace.Parallel
-- Init.MethodSpecsSimp
ShiftRight.shiftRight_hShiftRight : ∀ {α : Type u_1} [inst : ShiftRight α], ShiftRight.shiftRight = HShiftRight.hShiftRight
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.finrank_eq_four : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] [StrongRankCondition R],
  Module.finrank R (QuaternionAlgebra R c₁ c₂ c₃) = 4
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.uniq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MorphismProperty.LeftFraction.Localization W) E),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₁ =
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).comp F₂ →
    F₁ = F₂
-- Lean.Parser.Extension
Lean.Parser.AliasTable : Type → Type
-- Mathlib.Data.Multiset.ZeroCons
Multiset.mem_cons_of_mem : ∀ {α : Type u_1} {a b : α} {s : Multiset α}, a ∈ s → a ∈ b ::ₘ s
-- Mathlib.Order.Defs.Unbundled
/-- `Std.Total` as a definition, suitable for use in proofs.  -/
Total : {α : Sort u_1} → (α → α → Prop) → Prop
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosure.isSeparable : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra k K] [IsSepClosure k K],
  Algebra.IsSeparable k K
-- Batteries.Control.AlternativeMonad
AlternativeMonad.toMonad : {m : Type u_1 → Type u_2} → [self : AlternativeMonad m] → Monad m
-- Init.NotationExtra
unexpandTSyntaxArray : Lean.PrettyPrinter.Unexpander
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.minimalPrimes_comap_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ {I J : Ideal S}, J ∈ I.minimalPrimes → Ideal.comap f J ∈ (Ideal.comap f I).minimalPrimes
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- If a set has a closed thickening with finite measure, then the measure of its `r`-closed
thickenings converges to the measure of its closure as `r` tends to `0`.  -/
tendsto_measure_cthickening : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∃ R > 0, μ (Metric.cthickening R s) ≠ ⊤) →
    Filter.Tendsto (fun r => μ (Metric.cthickening r s)) (nhds 0) (nhds (μ (closure s)))
-- Lean.DocString.Add
/-- Parses a docstring as Verso, returning the syntax if successful.

When not successful, parser errors are logged.
 -/
Lean.parseVersoDocString : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadFileMap m] →
      [Lean.MonadError m] →
        [Lean.MonadEnv m] →
          [Lean.MonadOptions m] →
            [Lean.MonadLog m] →
              [Lean.MonadResolveName m] →
                Lean.TSyntax [`Lean.Parser.Command.docComment, `Lean.Parser.Command.moduleDoc] → m (Option Lean.Syntax)
-- Mathlib.CategoryTheory.Sites.PreservesLimits
instPreservesColimitSheafTypeUliftYonedaOfPreservesLimitOppositeOpObjFunctorIsSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : J.Subcanonical] {K : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} K]
  {F : CategoryTheory.Functor K C}
  [∀ (X : CategoryTheory.Sheaf J (Type (max v v'))), CategoryTheory.Limits.PreservesLimit F.op X.obj],
  CategoryTheory.Limits.PreservesColimit F (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_natCast_le_mul_natCast : ∀ {n : ℕ} {a b : Cardinal.{u_1}}, n ≠ 0 → (a * ↑n ≤ b * ↑n ↔ a ≤ b)
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SupSet α] [inst_1 : SupSet β] [inst_2 : SupSet γ]
  (f : sSupHom β γ) (g : sSupHom α β) (a : α), (f.comp g) a = f (g a)
-- Lean.Parser.Term
Lean.Parser.Term.logNamedWarningAtMacro.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.neg_hom_apply : ∀ {X Y : AddCommGrpCat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Data.Nat.Bits
/-- `shiftLeft' b m n` performs a left shift of `m` `n` times
and adds the bit `b` as the least significant bit each time.
Returns the corresponding natural number  -/
Nat.shiftLeft' : Bool → ℕ → ℕ → ℕ
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.struct.sizeOf_spec : ∀ (leanTypeName : Option Lean.Name) (types : Array Lean.IR.IRType),
  sizeOf (Lean.IR.IRType.struct leanTypeName types) = 1 + sizeOf leanTypeName + sizeOf types
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates limits, and `D` has all limits, then `C` has all limits.  -/
CategoryTheory.hasLimits_of_hasLimits_createsLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} D]
  [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} C
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α} [inst_1 : Inhabited ((a : α) × β a)],
  Std.Internal.List.getEntry! a l = (Std.Internal.List.getEntry? a l).get!
-- Mathlib.Tactic.DefEqAbuse
/-- > **WARNING:** `#defeq_abuse` is an experimental tool intended to assist with breaking
changes to transparency handling. Its syntax may change at any time, and it may not behave as
expected. Please report unexpected behavior [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency/with/575685551).

`#defeq_abuse in cmd` runs `cmd` with `backward.isDefEq.respectTransparency` both `true` and
`false`. If the command succeeds with `false` but fails with `true`, it identifies the specific
synthesis applications and `isDefEq` checks that fail with the stricter setting.

This is useful for diagnosing `instance` declarations or other commands where type class synthesis
failures occur during elaboration rather than within a tactic.

The command is re-executed with the permissive setting so that it actually takes effect.
 -/
Mathlib.Tactic.DefEqAbuse.defeqAbuseCmd : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- We say that a measurable space is countably separated if there is a
countable sequence of measurable sets separating points.  -/
MeasurableSpace.CountablySeparated : (α : Type u_3) → [MeasurableSpace α] → Prop
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- A slight variant of `hasDerivAt_of_tendstoLocallyUniformlyOn` with the assumption stated in
terms of `DifferentiableOn` rather than `HasDerivAt`. This makes a few proofs nicer in complex
analysis where holomorphicity is assumed but the derivative is not known a priori.  -/
hasDerivAt_of_tendsto_locally_uniformly_on' : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g g' : 𝕜 → G} {x : 𝕜}
  [IsRCLikeNormedField 𝕜] [l.NeBot] {s : Set 𝕜},
  IsOpen s →
    TendstoLocallyUniformlyOn (deriv ∘ f) g' l s →
      (∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x
-- Mathlib.Order.Hom.Basic
OrderIso.ofUnique_symm_apply : ∀ (α : Type u_6) (β : Type u_7) [inst : Unique α] [inst_1 : Unique β] [inst_2 : Preorder α] [inst_3 : Preorder β]
  (a : β), (RelIso.symm (OrderIso.ofUnique α β)) a = default
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_2 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, Nat.Partrec.Code.zero with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_2 k
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.instInhabitedApplyAtKey : Inhabited Mathlib.Tactic.ClickSuggestions.ApplyAtKey
-- Mathlib.Data.NNReal.Basic
NNReal.instFloorSemiring : FloorSemiring NNReal
-- Mathlib.Order.Bounds.Image
BddBelow.bddAbove_image2_of_bddAbove : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → BddBelow s → BddAbove t → BddAbove (Set.image2 f s t)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerveMap_app : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D) (x : SimplexCategoryᵒᵖ),
  (CategoryTheory.nerveMap F).app x = TypeCat.ofHom fun X => (F.mapComposableArrows (Opposite.unop x).len).obj X
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] →
                          FunLike (LeftInvariantDerivation I G) (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
                            (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
-- Mathlib.LinearAlgebra.Pi
LinearMap.ker_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι), (LinearMap.single R φ i).ker = ⊥
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Theory.Model.mk : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {T : L.Theory}, (∀ φ ∈ T, M ⊨ φ) → M ⊨ T
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNormedAddCommGroup : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [StarOrderedRing A] →
        {m : Type u_2} → {n : Type u_3} → [Fintype m] → [Fintype n] → NormedAddCommGroup (CStarMatrix m n A)