mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Graph
/-- The type of relations for the language of graphs, consisting of a single binary relation `adj`.
 -/
FirstOrder.Language.graphRel : ℕ → Type
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_equiv_eq_map_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : β ≃o α)
  (L : BooleanSubalgebra α),
  BooleanSubalgebra.comap
      (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L =
    BooleanSubalgebra.map
      (let __src := { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
      L
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarAlgHom_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) (a : A₁),
  e.toStarAlgHom a = e a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `Submodule.subtype` as a `LinearIsometry`.  -/
Submodule.subtypeₗᵢ : {E : Type u_5} →
  [inst : SeminormedAddCommGroup E] →
    {R' : Type u_11} → [inst_1 : Ring R'] → [inst_2 : Module R' E] → (p : Submodule R' E) → ↥p →ₗᵢ[R'] E
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst.sizeOf_spec : ∀ (x : Int.Internal.Linear.Var) (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.Data.ENat.Basic
ENat.lt_natCast_add_one_iff : ∀ {m : ℕ∞} {n : ℕ}, m < ↑n + 1 ↔ m ≤ ↑n
-- Mathlib.Combinatorics.Quiver.Symmetric
Prefunctor.MapReverse.mk : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver.HasReverse U]
  [inst_3 : Quiver.HasReverse V] {φ : U ⥤q V},
  (∀ {u v : U} (e : u ⟶ v), φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)) → φ.MapReverse
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Cover.trans.eq_1 : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j),
  𝒰.trans hij = AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hij
-- Mathlib.Order.Types.Defs
/-- The universe lift operation on order types. You can specify the universes explicitly with
`lift.{u, v} : OrderType.{v} → OrderType.{max v u}`  -/
OrderType.lift : OrderType.{v} → OrderType.{max v u}
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.lightToProfinite_map_proj_eq : ∀ (S : LightProfinite) (n : ℕ),
  lightToProfinite.map (S.proj n) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((CategoryTheory.Limits.IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj
        (Opposite.op n))
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_toInt64 : ∀ (x : Int8), x.toInt64.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Data.Sigma.Order
Sigma.Lex.denselyOrdered_of_noMaxOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), DenselyOrdered (α i)] [∀ (i : ι), NoMaxOrder (α i)], DenselyOrdered (Σₗ (i : ι), α i)
-- Lean.ExtraModUses
/-- Additional import dependency for elaboration.  -/
Lean.ExtraModUse : Type
-- Std.Time.Date.PlainDate
/-- Validates the date by ensuring that the year, month, and day form a correct and valid date.  -/
Std.Time.PlainDate.valid : ∀ (self : Std.Time.PlainDate), self.year.Valid self.month self.day
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C`, then the function is `C`-Lipschitz. Version with `HasDerivWithinAt`.  -/
Convex.norm_image_sub_le_of_norm_hasDerivWithin_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
  {f f' : 𝕜 → G} {s : Set 𝕜} {x y : 𝕜} {C : ℝ},
  (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
    (∀ x ∈ s, ‖f' x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Init.Data.List.Lemmas
List.foldr_eq_foldl_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β},
  List.foldr f b l = List.foldl (fun x y => f y x) b l.reverse
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Const.maxEntryD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α × β → α × β
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ioi_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.Iio b ∪ Set.Ioi a = Set.univ
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with multiplication. `TwoUniqueProds G` asserts that any two non-empty
finite subsets of `G`, at least one of which is not a singleton, possesses at least two pairs
of elements satisfying the `UniqueMul` property.  -/
TwoUniqueProds : (G : Type u_1) → [Mul G] → Prop
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.LaxMonoidal.whiskeringRight : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              [inst_4 : CategoryTheory.MonoidalCategory E] →
                (L : CategoryTheory.Functor D E) →
                  [L.LaxMonoidal] → ((CategoryTheory.Functor.whiskeringRight C D E).obj L).LaxMonoidal
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_add_right_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {c : ℝ},
  autoParam (‖f (min a b + c)‖ₑ ≠ ⊤) IntervalIntegrable.comp_add_right_iff._auto_1 →
    (IntervalIntegrable (fun x => f (x + c)) MeasureTheory.volume a b ↔
      IntervalIntegrable f MeasureTheory.volume (a + c) (b + c))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_mul_left : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {a : α}, (fun x => a * x) '' t = (fun x => a⁻¹ * x) ⁻¹' t
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of modules for style violations.
Print formatted errors for all unexpected style violations to standard output;
correct automatically fixable style errors if configured so.
Return the number of files which had new style errors.
`opts` contains the options defined in the Lakefile, determining which linters to enable.
`nolints` is a list of style exceptions to take into account.
`moduleNames` are the names of all the modules to lint,
`mode` specifies what kind of output this script should produce,
`fix` configures whether fixable errors should be corrected in-place.  -/
Mathlib.Linter.TextBased.lintModules : Lean.Linter.LinterOptions → Array String → Array Lean.Name → Mathlib.Linter.TextBased.ErrorFormat → Bool → IO UInt32
-- Lean.Compiler.ModPkgExt
/-- Returns the package \(if any\) of the current module.  -/
Lean.Environment.getModulePackage? : Lean.Environment → Option Lean.PkgId
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.NatTrans.leftDerived.eq_1 : ∀ {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.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  (α : F ⟶ G) (n : ℕ),
  CategoryTheory.NatTrans.leftDerived α n =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α)
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
-- Mathlib.Data.Rel
Set.image_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = (Function.graph f).image s
-- Lean.MetavarContext
/-- Revert the variables `xs` from the local context of `mvarId`, returning
an expression representing the (new) reverted metavariable and the list of
variables that were actually reverted (this list will include any forward dependencies).

See details in the comment at the top of the file.
 -/
Lean.MetavarContext.MkBinding.revert : Array Lean.Expr → Lean.MVarId → Lean.MetavarContext.MkBinding.M (Lean.Expr × Array Lean.Expr)
-- Mathlib.RingTheory.Valuation.Integers
/-- **Alias** of `Valuation.integer.coe_span_singleton_eq_setOfPred_le_v_coe`. -/
Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  (x : ↥v.integer), ↑(Ideal.span {x}) = {y | v ↑y ≤ v ↑x}
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.inf_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I),
  π₁ ⊓ π₂ = π₁.biUnion fun J => π₂.restrict J
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_norm_le' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), ‖a‖ - ‖b‖ ≤ ‖a / b‖
-- Mathlib.Topology.Compactness.Compact
/-- Finite topological spaces are compact.  -/
Finite.compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [Finite X], CompactSpace X
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddCommGrpCat.instBraidedForgetAddMonoidHomCarrier : (CategoryTheory.forget AddCommGrpCat).Braided
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Ico_succ_eq_of_Icc_eq : ∀ {m n : ℕ} {s : Finset ℕ}, Finset.Icc m n = s → Finset.Ico m (n + 1) = s
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.mk.injEq : ∀ (exact? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler)
  (children : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝))
  (wildcard? : Option Lean.Elab.ConfigEval.EvalConfigItemHandler) (projFn? struct? : Option Lean.Name)
  (exact?_1 : Option Lean.Elab.ConfigEval.EvalConfigItemHandler)
  (children_1 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝))
  (wildcard?_1 : Option Lean.Elab.ConfigEval.EvalConfigItemHandler) (projFn?_1 struct?_1 : Option Lean.Name),
  ({ exact? := exact?, children := children, wildcard? := wildcard?, projFn? := projFn?, struct? := struct? } =
      { exact? := exact?_1, children := children_1, wildcard? := wildcard?_1, projFn? := projFn?_1,
        struct? := struct?_1 }) =
    (exact? = exact?_1 ∧ children = children_1 ∧ wildcard? = wildcard?_1 ∧ projFn? = projFn?_1 ∧ struct? = struct?_1)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- When `η` is a finite kernel, `borelMarkovFromReal Ω η` is a finite kernel.  -/
ProbabilityTheory.Kernel.instIsFiniteKernelBorelMarkovFromReal : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (η : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsFiniteKernel η],
  ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η)
-- Mathlib.Computability.DFA
/-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state.  -/
DFA.accepts : {α : Type u} → {σ : Type v} → DFA α σ → Language α
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.supportWithinDomain : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (D : Function.locallyFinsuppWithin U Y), D.support ⊆ U
-- Mathlib.Topology.Semicontinuity.Defs
HasOpenLowerSections.lowerHemicontinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  HasOpenLowerSections f → LowerHemicontinuous f
-- Mathlib.CategoryTheory.Functor.Functorial
/-- Bundle a functorial function as a functor.
 -/
CategoryTheory.Functor.of : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : C → D) → [I : CategoryTheory.Functorial F] → CategoryTheory.Functor C D
-- Mathlib.Algebra.Order.Hom.Basic
map_sub_le_add : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupSeminormClass F α β] (f : F) (x y : α), f (x - y) ≤ f x + f y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeConnected_add_one : ∀ {V : Type u_1} {G : SimpleGraph V} {k : ℕ},
  k ≠ 0 → (G.IsEdgeConnected (k + 1) ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).IsEdgeConnected k)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split_ineq : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ) (b : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_left_split ctx p₁ p₂ k →
    Int.Internal.Linear.cooper_left_split_ineq_cert p₁ p₂ (↑k) b p' = true → Int.Internal.Linear.Poly.denote' ctx p' ≤ 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ext : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {p q : SkewMonoidAlgebra k G},
  (∀ (a : G), p.coeff a = q.coeff a) → p = q
-- Init.Data.Array.Lemmas
/-- Variant of `all_filter` with a side condition for the `stop` argument.  -/
Array.all_filter' : ∀ {α : Type u_1} {stop : ℕ} {xs : Array α} {p q : α → Bool},
  stop = (Array.filter p xs).size → (Array.filter p xs).all q 0 stop = xs.all fun a => !p a || q a
-- Lean.Meta.Closure
Lean.Meta.Closure.State.mk.inj : ∀ {visitedLevel : Lean.LevelMap Lean.Level} {visitedExpr : Lean.ExprStructMap Lean.Expr} {levelParams : Array Lean.Name}
  {nextLevelIdx : ℕ} {levelArgs : Array Lean.Level}
  {newLocalDecls newLocalDeclsForMVars newLetDecls : Array Lean.LocalDecl} {nextExprIdx : ℕ}
  {exprMVarArgs exprFVarArgs : Array Lean.Expr} {toProcess : Array Lean.Meta.Closure.ToProcessElement}
  {visitedLevel_1 : Lean.LevelMap Lean.Level} {visitedExpr_1 : Lean.ExprStructMap Lean.Expr}
  {levelParams_1 : Array Lean.Name} {nextLevelIdx_1 : ℕ} {levelArgs_1 : Array Lean.Level}
  {newLocalDecls_1 newLocalDeclsForMVars_1 newLetDecls_1 : Array Lean.LocalDecl} {nextExprIdx_1 : ℕ}
  {exprMVarArgs_1 exprFVarArgs_1 : Array Lean.Expr} {toProcess_1 : Array Lean.Meta.Closure.ToProcessElement},
  { visitedLevel := visitedLevel, visitedExpr := visitedExpr, levelParams := levelParams, nextLevelIdx := nextLevelIdx,
        levelArgs := levelArgs, newLocalDecls := newLocalDecls, newLocalDeclsForMVars := newLocalDeclsForMVars,
        newLetDecls := newLetDecls, nextExprIdx := nextExprIdx, exprMVarArgs := exprMVarArgs,
        exprFVarArgs := exprFVarArgs, toProcess := toProcess } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, levelParams := levelParams_1,
        nextLevelIdx := nextLevelIdx_1, levelArgs := levelArgs_1, newLocalDecls := newLocalDecls_1,
        newLocalDeclsForMVars := newLocalDeclsForMVars_1, newLetDecls := newLetDecls_1, nextExprIdx := nextExprIdx_1,
        exprMVarArgs := exprMVarArgs_1, exprFVarArgs := exprFVarArgs_1, toProcess := toProcess_1 } →
    visitedLevel = visitedLevel_1 ∧
      visitedExpr = visitedExpr_1 ∧
        levelParams = levelParams_1 ∧
          nextLevelIdx = nextLevelIdx_1 ∧
            levelArgs = levelArgs_1 ∧
              newLocalDecls = newLocalDecls_1 ∧
                newLocalDeclsForMVars = newLocalDeclsForMVars_1 ∧
                  newLetDecls = newLetDecls_1 ∧
                    nextExprIdx = nextExprIdx_1 ∧
                      exprMVarArgs = exprMVarArgs_1 ∧ exprFVarArgs = exprFVarArgs_1 ∧ toProcess = toProcess_1
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is left distributive over addition  -/
LeftDistribClass.left_distrib : ∀ {R : Type u_1} {inst : Mul R} {inst_1 : Add R} [self : LeftDistribClass R] (a b c : R), a * (b + c) = a * b + a * c
-- Lean.Exception
Lean.instMonadRecDepthStateRefT'OfMonad : {m : Type → Type} → {ω σ : Type} → [Monad m] → [Lean.MonadRecDepth m] → Lean.MonadRecDepth (StateRefT' ω σ m)
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- The diameter is the greatest distance between any two vertices, with the value `0` in
case the distances are not bounded above, or the graph is not connected.
 -/
SimpleGraph.diam : {α : Type u_1} → SimpleGraph α → ℕ
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.toSetoid_eq_bot : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M}, c.toSetoid = ⊥ ↔ c = ⊥
-- Mathlib.Data.Stream.Init
Stream'.head_map : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' α), (Stream'.map f s).head = f s.head
-- Mathlib.Topology.Order.IntermediateValue
IsTotallyDisconnected.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (s : Set α),
  IsTotallyDisconnected s = ∀ t ⊆ s, IsPreconnected t → t.Subsingleton
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mk_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Function.Surjective ⇑AddMonoid.Coprod.mk
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toLinearMap_injective : ∀ {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₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂], Function.Injective LinearIsometry.toLinearMap
-- Mathlib.GroupTheory.Coset.Defs
/-- The canonical map from an `AddGroup` `α` to the quotient `α ⧸ s`.  -/
QuotientAddGroup.mk : {α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → α → α ⧸ s
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
/-- A function `f : α × β → StieltjesFunction ℝ` is called a conditional kernel CDF of `κ` with
respect to `ν` if it is measurable, tends to 0 at -∞ and to 1 at +∞ for all `p : α × β`,
`fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ` and for all
measurable sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a).real (s ×ˢ Iic x)`.  -/
ProbabilityTheory.IsCondKernelCDF : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (α × β → StieltjesFunction ℝ) → ProbabilityTheory.Kernel α (β × ℝ) → ProbabilityTheory.Kernel α β → Prop
-- Lean.Attributes
Lean.AttributeApplicationTime.afterCompilation.sizeOf_spec : sizeOf Lean.AttributeApplicationTime.afterCompilation = 1
-- Lean.Elab.Tactic.Simp
/-- For equational theorems, usedTheorems record the declaration name. So if the user
specified `foo.eq_1`, we get `foo` in `usedTheorems`, but we still want to mark
`foo.eq_1` as used.
(cf. `recordSimpTheorem`)
This may lead to unused, explicitly given `foo.eq_1` to not be warned about. Ok for now,
eventually `recordSimpTheorem` could record the actual theorem, and the logic for
treating `foo.eq_1` as `foo` be moved to `SimpTrace.lean`
 -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.warnUnusedSimpArgs.usedThmIdOfSimpTheorem : Lean.Meta.SimpTheorem → Lean.MetaM Lean.Meta.Origin
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Right component of the associator as a 2-isomorphism in `Cat`.  -/
CategoryTheory.Bicategory.associatorNatIsoRightCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (d : B) →
            (CategoryTheory.Bicategory.precomposingCat a c d).obj (CategoryTheory.CategoryStruct.comp f g) ≅
              CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.precomposingCat b c d).obj g)
                ((CategoryTheory.Bicategory.precomposingCat a b d).obj f)
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_eq_card_filter : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  s.addEnergy t = {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 + x.1.2 = x.2.1 + x.2.2}.card
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap.eq_1 : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂],
  Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂ =
    {
      toFun := fun p =>
        (p.proj,
          (Bundle.Trivialization.continuousLinearMapAt 𝕜 e₂ p.proj).compContinuousAlternatingMap
            (p.snd.compContinuousLinearMap (Bundle.Trivialization.symmL 𝕜 e₁ p.proj))),
      invFun := fun p =>
        ⟨p.1,
          (Bundle.Trivialization.symmL 𝕜 e₂ p.1).compContinuousAlternatingMap
            (p.2.compContinuousLinearMap (Bundle.Trivialization.continuousLinearMapAt 𝕜 e₁ p.1))⟩,
      source := Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_target := ⋯,
      baseSet := e₁.baseSet ∩ e₂.baseSet, open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.prodMap : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [inst_1 : UniformSpace β'] {F' : ι' → α' → β'}
  {f' : α' → β'} {q : Filter ι'} {q' : Filter α'},
  TendstoUniformlyOnFilter F f p p' →
    TendstoUniformlyOnFilter F' f' q q' →
      TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.ε.eq_1 : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  Rep.standardComplex.ε k G =
    Rep.ofHom
      { toLinearMap := (Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
        isIntertwining' := ⋯ }
-- Init.Data.Vector.Lemmas
Vector.eq_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {as : Array α} {h : as.size = n}, xs = Vector.mk as h ↔ xs.toArray = as
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅},
  t.get? (t.min he) = some (t.min he)
-- Mathlib.Algebra.GroupWithZero.Action.Basic
MulAction.bijective₀ : ∀ {G₀ : Type u_2} {α : Type u_8} [inst : GroupWithZero G₀] [inst_1 : MulAction G₀ α] {a : G₀},
  a ≠ 0 → Function.Bijective fun x => a • x
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMap_comp_map : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (n m k : ℕ)
  (hn : n = m + k),
  (MvPolynomial.universalFactorizationMap S n m k hn).comp (MvPolynomial.map (algebraMap R S)) =
    (Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (MvPolynomial.mapAlgHom (Algebra.ofId R S)))
          ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp
            (MvPolynomial.mapAlgHom (Algebra.ofId R S)))
          ⋯).comp
      (MvPolynomial.universalFactorizationMap R n m k hn).toRingHom