mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.CoreM
/-- Returns the current set of tasks added by `logSnapshotTask` and then resets it. When
saving/restoring state of an action that may have logged such tasks during incremental reuse, this
function must be used to store them in the corresponding snapshot tree; otherwise, they will leak
outside and may be cancelled by a later step, potentially leading to inconsistent state being
reused.
 -/
Lean.Core.getAndEmptySnapshotTasks : Lean.CoreM (Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree))
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- A differential ring `A` and an algebra over it `B` share constants if all
constants in B are in the range of `algebraMap A B`.
 -/
Differential.ContainConstants : (A : Type u_1) → (B : Type u_2) → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → [Differential B] → Prop
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
of transfinite compositions of pushouts of coproducts of maps in `I`.  -/
CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  I.rlp.llp =
    (CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u}
        (CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts).retracts
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A), S.toNonUnitalStarSubalgebra ⋯ = S
-- Lean.Elab.Attributes
Lean.Elab.Attribute : Type
-- Mathlib.Data.List.Sigma
List.nodupKeys_middle : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} {s : Sigma β},
  (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys
-- Init.Data.Fin.Lemmas
Fin.induction.go : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_1} →
    motive 0 → ((i : Fin n) → motive i.castSucc → motive i.succ) → (i : ℕ) → (hi : i < n + 1) → motive ⟨i, hi⟩
-- Mathlib.Tactic.ITauto
/-- Constructor for `p ↔ q`.  -/
Mathlib.Tactic.ITauto.IProp.iff : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Combinatorics.SetFamily.Intersecting
/-- Maximal intersecting families are upper sets. Finset version.  -/
Set.Intersecting.isUpperSet' : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Finset α},
  (↑s).Intersecting → (∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) → IsUpperSet ↑s
-- Mathlib.Topology.Algebra.UniformConvergence
instCommGroupUniformFun : {α : Type u_1} → {β : Type u_2} → [CommGroup β] → CommGroup (UniformFun α β)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], OrderDual.instZero = inst
-- Mathlib.Data.Set.UnionLift
Set.iUnionLift_inclusion : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  {hT : T ⊆ Set.iUnion S} {i : ι} (x : ↑(S i)) (h : S i ⊆ T), Set.iUnionLift S f hf T hT (Set.inclusion h x) = f i x
-- Mathlib.Topology.Connected.Basic
/-- The image of a preconnected set is preconnected as well.  -/
IsPreconnected.image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α},
  IsPreconnected s → ∀ (f : α → β), ContinuousOn f s → IsPreconnected (f '' s)
-- Init.Data.Format.Syntax
Lean.Syntax.formatStxAux : Option ℕ → Bool → ℕ → Lean.Syntax → Std.Format
-- Mathlib.Data.ENNReal.Real
ENNReal.coe_lt_ofReal : ∀ {a : NNReal} {b : ℝ}, ↑a < ENNReal.ofReal b ↔ ↑a < b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGet?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.Const.get? t₁ k = Std.DTreeMap.Internal.Impl.Const.get? t₂ k
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModuleMap_hom_apply : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] {M N : ModuleCat R} (S : Submonoid R) (f : M ⟶ N)
  (a : ↑(M.localizedModule S)),
  (ModuleCat.Hom.hom (ModuleCat.localizedModuleMap S f)) a =
    ((IsLocalizedModule.map S (M.localizedModuleMkLinearMap S) (N.localizedModuleMkLinearMap S)) (ModuleCat.Hom.hom f))
      a
-- Std.Time.DateTime.PlainDateTime
/-- Sets the `PlainDateTime` to the specified `Weekday`.
 -/
Std.Time.PlainDateTime.withWeekday : Std.Time.PlainDateTime → Std.Time.Weekday → Std.Time.PlainDateTime
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α},
      List.Pairwise (fun a b => (a == b) = false) l →
        (∀ (a : α), m.contains a = true → l.contains a = false) →
          (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).size = (↑m).size + l.length
-- Mathlib.Topology.Order
discreteTopology_iff_forall_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α], DiscreteTopology α ↔ ∀ (s : Set α), IsOpen s
-- Lean.Parser.Basic
Lean.Parser.trailingNode : Lean.SyntaxNodeKind → ℕ → ℕ → Lean.Parser.Parser → Lean.Parser.TrailingParser
-- Mathlib.FieldTheory.JacobsonNoether
_private.Mathlib.FieldTheory.JacobsonNoether.0.JacobsonNoether.termK : Lean.ParserDescr
-- Init.Data.String.Defs
ByteArray.isValidUTF8_utf8Encode : ∀ {l : List Char}, l.utf8Encode.IsValidUTF8
-- Init.Data.Vector.Lemmas
Vector.findM?_mk : ∀ {m : Type → Type} {α : Type} {n : ℕ} [inst : Monad m] {xs : Array α} (h : xs.size = n) (f : α → m Bool),
  Vector.findM? f (Vector.mk xs h) = Array.findM? f xs
-- Lean.Elab.Tactic.Ext
/-- Apply a single extensionality theorem to the current goal.  -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.evalApplyExtTheorem : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.indicatorConstLp_univ : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  MeasureTheory.indicatorConstLp p ⋯ ⋯ c = (MeasureTheory.Lp.const p μ) c
-- Mathlib.RingTheory.Conductor
conductor_eq_top_of_powerBasis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S),
  conductor R pb.gen = ⊤
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.brecOn.eq : ∀ {m : Type u → Type u} {α : Type u} {motive_1 : MLList.MLListImpl✝ m α → Sort u_1}
  {motive_2 : Thunk (MLList.MLListImpl✝ m α) → Sort u_1} (t : MLList.MLListImpl✝ m α)
  (F_1 : (t : MLList.MLListImpl✝ m α) → MLList.MLListImpl.below✝ t → motive_1 t)
  (F_2 : (t : Thunk (MLList.MLListImpl✝ m α)) → MLList.MLListImpl.below_1✝ t → motive_2 t),
  MLList.MLListImpl.brecOn✝ t F_1 F_2 = F_1 t (MLList.MLListImpl.brecOn.go✝ t F_1 F_2).2
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
algebraMap_isIntegral_iff : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  (algebraMap R A).IsIntegral ↔ Algebra.IsIntegral R A
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instInf : {α : Type u_1} → [inst : TopologicalSpace α] → [QuasiSeparatedSpace α] → Min (TopologicalSpace.CompactOpens α)
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges.congr_simp : ∀ {α : Type u_4} {β : Type u_5} (r r_1 : α → β → Prop),
  r = r_1 →
    ∀ {inst : (a : α) → DecidablePred (r a)} [inst_1 : (a : α) → DecidablePred (r_1 a)] (s s_1 : Finset α),
      s = s_1 → ∀ (t t_1 : Finset β), t = t_1 → Rel.interedges r s t = Rel.interedges r_1 s_1 t_1
-- Mathlib.Data.Rat.Init
/-- Typeclass for the canonical homomorphism `ℚ≥0 → K`.

This should be considered as a notation typeclass. The sole purpose of this typeclass is to be
extended by `DivisionSemiring`.  -/
NNRatCast : Type u_1 → Type u_1
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mk : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : Ring 𝕜] →
      [inst_1 : PartialOrder 𝕜] →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex E) →
              (∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex.faces → AffineIndependent 𝕜 Subtype.val) →
                (∀ {s t : Finset E},
                    s ∈ toPreAbstractSimplicialComplex.faces →
                      t ∈ toPreAbstractSimplicialComplex.faces →
                        (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)) →
                  Geometry.SimplicialComplex 𝕜 E
-- Mathlib.Order.ModularLattice
le_iff_eq_of_codisjoint_of_disjoint : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α] {a b c : α},
  Codisjoint a b → Disjoint b c → (a ≤ c ↔ a = c)
-- Mathlib.Topology.Connected.PathConnected
mem_pathComponent_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ∈ pathComponent y ↔ Joined y x
-- Init.Data.List.Attach
List.tail_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a),
  (List.pmap f xs H).tail = List.pmap f xs.tail ⋯
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift_comp_inlHom : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r),
  (TrivSqZeroExt.lift f g hg hfg hgf).comp (TrivSqZeroExt.inlAlgHom S R M) = f
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The discriminant is invariant under `T : z ↦ z + 1`, i.e., `Δ(z + 1) = Δ(z)`.  -/
ModularForm.discriminant_T_invariant : SlashAction.map 12 ModularGroup.T ModularForm.discriminant = ModularForm.discriminant
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
/-- Convergence in probability (`TendstoInMeasure`) implies convergence in distribution
(`TendstoInDistribution`).  -/
MeasureTheory.TendstoInMeasure.tendstoInDistribution_of_aemeasurable : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst : MeasureTheory.IsProbabilityMeasure μ'] {mE : MeasurableSpace E} {Z : Ω' → E} {l : Filter ι}
  [inst_1 : SeminormedAddCommGroup E] [SecondCountableTopology E] [inst_3 : BorelSpace E] [l.IsCountablyGenerated]
  {X : ι → Ω' → E},
  MeasureTheory.TendstoInMeasure μ' X l Z →
    (∀ (i : ι), AEMeasurable (X i) μ') → AEMeasurable Z μ' → MeasureTheory.TendstoInDistribution X l Z (fun x => μ') μ'
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instInhabited : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Inhabited (FreeAlgebra R X)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- A bit-vector literal  -/
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.Literal : Type
-- Init.Meta.Defs
Lean.Meta.Rewrite.Config.mk : Lean.Meta.TransparencyMode → Bool → Lean.Meta.Occurrences → Lean.Meta.Rewrite.NewGoals → Lean.Meta.Rewrite.Config
-- Mathlib.Order.Monotone.Basic
StrictMono.compares : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α} {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piCongrLeft_symm_apply : ∀ {ι : Type u_2} {ι' : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] {Y : ι' → Type u_4}
  [inst_2 : (j : ι') → PseudoEMetricSpace (Y j)] (e : ι ≃ ι') (a : (i : ι') → Y i) (j : ι),
  (IsometryEquiv.piCongrLeft e).symm a j = a (e j)
-- Mathlib.Order.WithBot
/-- There is a general version `le_bot_iff`, but this lemma does not require a `PartialOrder`.  -/
WithBot.le_bot_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithBot α}, x ≤ ⊥ ↔ x = ⊥
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.DTreeMap.getKeyLE! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α → α
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns a `List` of the key/value pairs in order.  -/
Std.DTreeMap.Internal.Impl.Const.toArray : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → Array (α × β)
-- Init.Meta.Defs
Lean.Syntax.instCoeTermTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe Lean.Term (Lean.TSyntax `Lean.Parser.Term.funBinder)
-- Mathlib.Computability.NFA
/-- `M.toDFA` is a `DFA` constructed from an `NFA` `M` using the subset construction. The
states is the type of `Set`s of `M.state` and the step function is `M.stepSet`.  -/
NFA.toDFA : {α : Type u} → {σ : Type v} → NFA α σ → DFA α (Set σ)
-- Mathlib.CategoryTheory.Subobject.WellPowered
CategoryTheory.wellPowered_of_smallCategory : ∀ (C : Type u₁) [inst : CategoryTheory.SmallCategory C], CategoryTheory.WellPowered.{u₁, u₁, u₁} C
-- Init.Data.UInt.Lemmas
USize.toUInt64_inj : ∀ {a b : USize}, a.toUInt64 = b.toUInt64 ↔ a = b
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.mk.sizeOf_spec : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  [inst_9 : SizeOf k] [inst_10 : SizeOf P₁] [inst_11 : SizeOf P₂] [inst_12 : SizeOf V₁] [inst_13 : SizeOf V₂]
  (toAffineEquiv : P₁ ≃ᵃ[k] P₂)
  (continuous_toFun : autoParam (Continuous toAffineEquiv.toFun) ContinuousAffineEquiv.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAffineEquiv.invFun) ContinuousAffineEquiv.continuous_invFun._autoParam),
  sizeOf
      { toAffineEquiv := toAffineEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toAffineEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Mathlib.Logic.Relation
Relation.ReflTransGen.tail : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α}, Relation.ReflTransGen r a b → r b c → Relation.ReflTransGen r a c
-- Init.Data.Ord.Basic
Ordering.exists : ∀ {p : Ordering → Prop}, (∃ o, p o) ↔ p Ordering.lt ∨ p Ordering.eq ∨ p Ordering.gt
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The bijection between the free group on a singleton, and the integers.  -/
FreeGroup.freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.coe_toEnd : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) (x : L) (y : ↥N), ↑(((LieModule.toEnd R L ↥N) x) y) = ((LieModule.toEnd R L M) x) ↑y
-- Lean.Environment
Lean.MonadEnv : (Type → Type) → Type
-- Mathlib.Combinatorics.Nullstellensatz
/-- The degree of `Alon.P S i` with respect to `X i` is the cardinality of `S`,
and `0` otherwise.  -/
_private.Mathlib.Combinatorics.Nullstellensatz.0.MvPolynomial.Alon.degree_P : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Nontrivial R] (m : MonomialOrder σ) (S : Finset R) (i : σ),
  m.degree (MvPolynomial.Alon.P✝ S i) = fun₀ | i => S.card
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.eq_def : ∀ {α : Type u_1} (p : α → Bool) (x x_1 : List α),
  List.splitOnPPrepend p x x_1 =
    match x, x_1 with
    | [], acc => [acc.reverse]
    | a :: t, acc =>
      if p a = true then acc.reverse :: List.splitOnPPrepend p t [] else List.splitOnPPrepend p t (a :: acc)
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_rhs_exact : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) (lhs₁ rhs₁ lhs₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
    Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx lhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₁
-- Mathlib.Algebra.Order.GroupWithZero.Lex
MonoidWithZeroHom.inl_mono : ∀ {M₀ : Type u_1} {N₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero M₀] [inst_1 : GroupWithZero N₀]
  [inst_2 : Preorder N₀] [inst_3 : DecidablePred fun x => x = 0], Monotone ⇑(MonoidWithZeroHom.inl M₀ N₀)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → km ∈ t
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mk : {X Y : AlgebraicGeometry.Scheme} → (domain : X.Opens) → Dense ↑domain → (↑domain ⟶ Y) → X.PartialMap Y
-- Mathlib.Data.Sym.Basic
Sym.mem_cons : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n} {a b : α}, a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s
-- Init.Data.SInt.Basic
Int16.ofUInt16 : UInt16 → Int16
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instAddCommGroup : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → AddCommGroup (PolynomialModule R M)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given a "crown" of morphisms
```
  j₁   j₂   j₃  ... jₙ
 /  \  /\  /  \
|    \/  \/    |
|    /\  /\    |
|   |  \/  |   |
 \  |  /\  |  /
  \ | /  \ | /
   vvv    vvv
    k₁    k₂
```
in a filtered category, we can construct an object `s` and two morphisms from `k₁` and `k₂` to `s`,
making the resulting squares commute.
 -/
CategoryTheory.IsFiltered.crown : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {ι : Type u_1} [Finite ι]
  (j : ι → C) {k₁ k₂ : C} (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
  ∃ s α β, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) α = CategoryTheory.CategoryStruct.comp (g i) β
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.isFiniteMeasure_restrict_Icc : ∀ (x y : ℝ), MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Icc x y))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommAddMonObj.instTensorAddUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommAddMonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Http.Transport
/-- Gets the receive channel for a client (server to client direction).
 -/
Std.Http.Internal.Mock.Client.getRecvChan : Std.Http.Internal.Mock.Client → Std.CloseableChannel ByteArray
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.struc : {L : FirstOrder.Language} → {T : L.Theory} → (self : T.ModelType) → L.Structure ↑self
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- `Polynomial.Gal.restrict` for the composition of polynomials.  -/
Polynomial.Gal.restrictComp : {F : Type u_1} → [inst : Field F] → (p q : Polynomial F) → q.natDegree ≠ 0 → (p.comp q).Gal →* p.Gal
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.addSubgroupOf K = ⊥ ↔ Disjoint H K
-- Mathlib.Probability.Kernel.Basic
/-- Kernel with value `(κ a).comap f`, for a measurable embedding `f`. That is, for a measurable set
`t : Set β`, `ProbabilityTheory.Kernel.comapRight κ hf a t = κ a (f '' t)`.  -/
ProbabilityTheory.Kernel.comapRight : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            {f : γ → β} → ProbabilityTheory.Kernel α β → MeasurableEmbedding f → ProbabilityTheory.Kernel α γ
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume. Then the limit
as `n → ∞` of `card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι` tends to the volume of `s`. This is a
special case of `tendsto_card_div_pow` with `F = 1`.  -/
tendsto_card_div_pow_atTop_volume : ∀ {ι : Type u_1} (s : Set (ι → ℝ)) [inst : Fintype ι],
  Bornology.IsBounded s →
    MeasurableSet s →
      MeasureTheory.volume (frontier s) = 0 →
        Filter.Tendsto
          (fun n =>
            ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑(Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑n ^ Fintype.card ι)
          Filter.atTop (nhds (MeasureTheory.volume.real s))
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFullUlift : ∀ (R : Type u) [inst : Ring R], (FGModuleCat.ulift R).Full
-- Lean.Parser.Command
Lean.Parser.Command.whereStructInst : Lean.Parser.Parser
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_append : ∀ {α : Type u_1} (l₁ l₂ : Batteries.DList α), (l₁ ++ l₂).toList = l₁.toList ++ l₂.toList
-- Mathlib.Algebra.Quandle
Rack.envelAction_prop : ∀ {R : Type u_1} [inst : Rack R] (x y : R), (Rack.envelAction ((Rack.toEnvelGroup R) x)) y = Shelf.act x y
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.Finite.linearMap : ∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [inst_6 : AddCommGroup N] [inst_7 : Module R N]
  [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [Module.Finite S N], Module.Finite S (M →ₗ[R] N)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_toInt8 : ∀ (n : ISize) (h : System.Platform.numBits = 64), n.toInt8.toBitVec = BitVec.signExtend 8 (n.toBitVec64 h)
-- Mathlib.RingTheory.TensorProduct.Finite
Submodule.exists_fg_le_subset_range_rTensor_subtype : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (s : Set (TensorProduct R N M)),
  s.Finite → ∃ J, ∃ (_ : J.FG), s ⊆ ↑(LinearMap.rTensor M J.subtype).range
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit : ∀ {C : Type u} {F : C → Type v} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) (x : c.pt),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (c.inj i)) y = x
-- Init.Data.SInt.Lemmas
Int64.toBitVec_mul : ∀ {a b : Int64}, (a * b).toBitVec = a.toBitVec * b.toBitVec
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.homEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnrichedOrdinary C}
  (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.CatEnrichedOrdinary.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnrichedOrdinary.homEquiv f)
      (CategoryTheory.CatEnrichedOrdinary.homEquiv g)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.instMonoOfIsThin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [Quiver.IsThin C] (f : Y ⟶ X), CategoryTheory.Mono f
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ContinuousOn f (closure s)