mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The range of a ring homomorphism is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype S`.  -/
RingHom.fintypeRange : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] →
      [inst_1 : NonAssocRing S] → [Fintype R] → [DecidableEq S] → (f : R →+* S) → Fintype ↥f.range
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Any functor from a finite category to `Type*` that only involves finite objects,
has a finite colimit.  -/
CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] →
      (K : CategoryTheory.Functor J (Type u_1)) →
        [∀ (j : J), Finite (K.obj j)] → Fintype (CategoryTheory.Limits.colimit K)
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.fvarIds : Lean.CollectFVars.State → Array Lean.FVarId
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_lift_of_fintype : ∀ (α : Type u) (β : Type v) [inst : Fintype α] [inst_1 : Zero β],
  Cardinal.mk (α →₀ β) = Cardinal.lift.{u, v} (Cardinal.mk β) ^ Fintype.card α
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.isIso_πTruncGE_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C], CategoryTheory.IsIso (K.πTruncGE e) ↔ K.IsStrictlySupported e
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match 0 with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_1 ()
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (h : CategoryTheory.CategoryStruct.id X = 0),
  ((CategoryTheory.Limits.idZeroEquivIsoZero X) h).inv = 0
-- Mathlib.Data.Int.Init
Int.div_lt_div_iff_of_dvd_of_neg_of_neg : ∀ {a b c d : ℤ}, b < 0 → d < 0 → b ∣ a → d ∣ c → (a / b < c / d ↔ d * a < c * b)
-- Mathlib.LinearAlgebra.Matrix.Module
Matrix.Module.smul_def : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (N : Matrix ι ι R) (v : ι → M), N • v = fun i => ∑ j, N i j • v j
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.isCoatomic_submodule : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], IsCoatomic (Submodule R M)
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.of_comp_of_mem_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P],
  g ∘ f = 1 → (∀ (x : N), g x = 1 → x ∈ Set.range f) → Function.MulExact f g
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprodComparison.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)],
  CategoryTheory.Limits.coprodComparison F A B =
    CategoryTheory.Limits.coprod.desc (F.map CategoryTheory.Limits.coprod.inl) (F.map CategoryTheory.Limits.coprod.inr)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions of length three are preserved under semigroup homomorphisms.  -/
ThreeAPFree.image' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s : Set α}
  [inst_2 : FunLike F α β] [AddHomClass F α β] (f : F), Set.InjOn (⇑f) (s + s) → ThreeAPFree s → ThreeAPFree (⇑f '' s)
-- Std.Time.Date.Unit.Week
Std.Time.Week.instReprOrdinal : Repr Std.Time.Week.Ordinal
-- Mathlib.Algebra.Order.SuccPred
Order.le_of_sub_one_lt : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α], x - 1 < y → x ≤ y
-- Mathlib.NumberTheory.ModularForms.Basic
SlashInvariantForm.mk.congr_simp : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (toFun toFun_1 : UpperHalfPlane → ℂ) (e_toFun : toFun = toFun_1)
  (slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun),
  { toFun := toFun, slash_action_eq' := slash_action_eq' } = { toFun := toFun_1, slash_action_eq' := ⋯ }
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_surjective : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Function.Surjective ⇑(LinearMap.snd R M M₂)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.monic : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] (p : Polynomial.MonicDegreeEq R n), (↑p).Monic
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_support : ∀ {R : Type u_1} [inst : Semiring R] (N : ℕ) (f : Polynomial R),
  (Polynomial.reflect N f).support = Finset.image (⇑(Polynomial.revAt N)) f.support
-- Lean.Data.LBool
Lean.Bool.toLBool : Bool → Lean.LBool
-- Mathlib.Probability.Independence.Integration
/-- If `f` and `g` are independent random variables with values in `ℝ≥0∞`,
then `E[f * g] = E[f] * E[g]`.  -/
ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal},
  Measurable f →
    Measurable g →
      ProbabilityTheory.IndepFun f g μ → ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib.CategoryTheory.RepresentedBy
/-- If `F` is represented by `X` with universal element `x : F.obj X`, modulo universe
lifting, it is isomorphic to `yoneda.obj X`.  -/
CategoryTheory.Functor.IsRepresentedBy.uliftYonedaIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {x : F.obj (Opposite.op X)} →
          F.IsRepresentedBy x → (CategoryTheory.uliftYoneda.{w, v, u}.obj X ≅ F.comp CategoryTheory.uliftFunctor.{v, w})
-- Mathlib.Topology.LocallyFinsupp
/-- Simplifier lemma: coercion of `single x y` to a function.
 -/
Function.locallyFinsuppWithin.coe_single : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y] {x : X} {y : Y},
  ⇑(Function.locallyFinsuppWithin.single x y) = Pi.single x y
-- Mathlib.SetTheory.ZFC.Class
/-- `{x ∈ A | p x}` is the class of elements in `A` satisfying `p`  -/
Class.sep : (ZFSet.{u_1} → Prop) → Class.{u_1} → Class.{u_1}
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkWsBefore.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.height.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), I.height = ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), Ideal.primeHeight✝ J
-- Init.Data.List.MinMax
List.max?_eq_none_iff : ∀ {α : Type u_1} {xs : List α} [inst : Max α], xs.max? = none ↔ xs = []
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- Consider an additive group `G` acting on a measure space `X`.
A sequence of sets `F : ι → Set X` is **Følner** with respect to the `G`-action,
the measure `μ`, and a filter `l` on the indexing type `ι`, if:
1. Each `s` in `l` is eventually measurable with finite non-zero measure,
2. For all `g : G`, `μ ((g +ᵥ F i) ∆ F i) / μ (F i)` tends to `0`.  -/
IsAddFoelner : (G : Type u_4) →
  {X : Type u_5} →
    [inst : MeasurableSpace X] →
      MeasureTheory.Measure X → [inst : AddGroup G] → [AddAction G X] → {ι : Type u_6} → Filter ι → (ι → Set X) → Prop
-- Mathlib.Data.Sym.Sym2
Sym2.mem_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : Sym2 α}, b ∈ Sym2.map f z ↔ ∃ a ∈ z, f a = b
-- Mathlib.Data.Matrix.Composition
Matrix.comp_symm_diagonal : ∀ {I : Type u_1} {J : Type u_2} {R : Type u_5} [inst : DecidableEq I] [inst_1 : DecidableEq J] [inst_2 : Zero R]
  (d : I × J → R),
  (Matrix.comp I I J J R).symm (Matrix.diagonal d) = Matrix.diagonal fun i => Matrix.diagonal fun j => d (i, j)
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.sum_moebius_mul_log_eq : ∀ {n : ℕ},
  ∑ d ∈ n.divisors, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.log d = -ArithmeticFunction.vonMangoldt n
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLT?.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.gt) → ((x : Ordering) → (x = Ordering.gt → False) → motive x) → motive x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.strictAntiOn_logb_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → StrictAntiOn (Real.logb b) (Set.Ioi 0)
-- Mathlib.FieldTheory.Extension
/-- Let `K/F` be an algebraic extension of fields and `L` a field in which all the minimal
polynomial over `F` of elements of `K` splits. Then, for `x ∈ K`, the images of `x` by the
`F`-algebra morphisms from `K` to `L` are exactly the roots in `L` of the minimal polynomial
of `x` over `F`.  -/
Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits : ∀ {F : Type u_1} {K : Type u_2} (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F L] [inst_4 : Algebra F K],
  (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) →
    ∀ [Algebra.IsAlgebraic F K] (x : K), (Set.range fun ψ => ψ x) = (minpoly F x).rootSet L
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorObj_carrier : ∀ (R : Type u) [inst : CommRing R] (X Y : CoalgCat R),
  ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).toModuleCat = TensorProduct R ↑X.toModuleCat ↑Y.toModuleCat
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout`. -/
CategoryTheory.MorphismProperty.of_isPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'},
  CategoryTheory.IsPushout g f f' g' → P f → P f'
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonLogConfig.toJson : Lean.Lsp.LogConfig → Lean.Json
-- Std.Data.ExtDTreeMap.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.ExtDTreeMap.empty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.ExtDTreeMap α β cmp
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subRight_symm_apply : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x b : G),
  (Homeomorph.subRight x).symm b = b + x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_2 : ∀ (k : ℤ), (Lean.Grind.CommRing.Expr.intCast k).toPoly = Lean.Grind.CommRing.Poly.num k
-- Mathlib.Algebra.Notation.Indicator
/-- See `Set.eqOn_indicator'` for the version with `sᶜ`.  -/
Set.eqOn_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M}, Set.EqOn (s.indicator f) f s
-- Mathlib.Order.Types.Defs
/-- To define a function on `OrderType`, it suffices to define it on all linear orders.
 -/
OrderType.liftOn : {δ : Sort v} →
  OrderType.{u_1} →
    (f : (α : Type u_1) → [LinearOrder α] → δ) →
      (∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β],
          OrderType.type α = OrderType.type β → f α = f β) →
        δ
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.compactConvergenceUniformSpace.eq_1 : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β],
  ContinuousMap.compactConvergenceUniformSpace =
    (UniformSpace.comap ContinuousMap.toUniformOnFunIsCompact inferInstance).replaceTopology ⋯
-- Mathlib.Order.Interval.Finset.Nat
Nat.cauchy_induction_mul : ∀ {P : ℕ → Prop},
  (∀ (n : ℕ), P (n + 1) → P n) →
    ∀ (k seed : ℕ), 1 < k → P seed.succ → (∀ (x : ℕ), seed < x → P x → P (k * x)) → ∀ (n : ℕ), P n
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_eq_mul'_comp_mapIncl : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  M.mulMap N = LinearMap.mul' R S ∘ₗ TensorProduct.mapIncl M N
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_pos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν → ∀ᵐ (x : α) ∂μ, 0 < μ.rnDeriv ν x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NumberField.mixedEmbedding.logMap 0 = 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.invFun_eq_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f : M ≃+ N}, f.invFun = ⇑f.symm
-- Batteries.Data.List.Scan
List.partialSums_cons : ∀ {α : Type u_1} {a : α} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {l : List α},
  (a :: l).partialSums = 0 :: List.map (fun x => a + x) l.partialSums
-- Mathlib.Order.Interval.Finset.Defs
Prod.instLocallyFiniteOrderBot.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] [inst_4 : DecidableLE (α × β)],
  Prod.instLocallyFiniteOrderBot = LocallyFiniteOrderBot.ofIic' (α × β) (fun x => Finset.Iic x.1 ×ˢ Finset.Iic x.2) ⋯
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.eq_1 : ∀ {α : Type u_1} {ε : Type u_4} [inst : ENorm ε] {x : MeasurableSpace α} (f : α → ε) (μ : MeasureTheory.Measure α),
  MeasureTheory.HasFiniteIntegral f μ = (∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_congr : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)}
  {a b : α}, (a == b) = true → Std.Internal.List.getValue! a l = Std.Internal.List.getValue! b l
-- Mathlib.SetTheory.Ordinal.Exponential
/-- `opow b` and `log b` (almost) form a Galois connection.

See `opow_le_iff_le_log` for a variant assuming `x ≠ 0` rather than `c ≠ 0`. See also
`le_log_of_opow_le` and `opow_le_of_le_log`, which are both separate implications under weaker
assumptions.  -/
Ordinal.opow_le_iff_le_log' : ∀ {b x c : Ordinal.{u_1}}, 1 < b → c ≠ 0 → (b ^ c ≤ x ↔ c ≤ Ordinal.log b x)
-- Std.Sat.AIG.CachedLemmas
/-- `AIG.mkGateCached` never shrinks the underlying AIG.
 -/
Std.Sat.AIG.mkGateCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size
-- Lean.Elab.MutualInductive
/-- Auxiliary function for `inferResultingUniverse`. Applies `accLevelAtCtor` to each constructor.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.collectUniverseConstraints : Array Lean.Elab.Command.InductiveView →
  Lean.Level →
    ℕ → ℕ → List Lean.InductiveType → Array Lean.LMVarId → Lean.Elab.TermElabM Lean.Elab.Command.AccLevelState✝
-- Mathlib.Order.Height
Set.encard_eq_chainHeight_of_isChain : ∀ {α : Type u_1} {r : α → α → Prop} (s : Set α), IsChain r s → s.encard = s.chainHeight r
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.iCondIndepFun_indicator : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : Zero β] [inst_3 : One β]
  {m : MeasurableSpace β} {s : ι → Set Ω},
  ProbabilityTheory.iCondIndepSet m' hm' s μ →
    ProbabilityTheory.iCondIndepFun m' hm' (fun n => (s n).indicator fun _ω => 1) μ
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Given a kernel pair of an effective epimorphism `f : X ⟶ B`, the induced cofork is a coequalizer.
 -/
CategoryTheory.isColimitCoforkOfEffectiveEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B X : C} →
      (f : X ⟶ B) →
        [CategoryTheory.EffectiveEpi f] →
          (c : CategoryTheory.Limits.PullbackCone f f) →
            CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)
-- Batteries.Recycling.RBTree.Basic
/-- An `RBSet` is a self-balancing binary search tree.
The `cmp` function is the comparator that will be used for performing searches;
it should satisfy the requirements of `TransCmp` for it to have sensible behavior.
 -/
RBTree.RBSet : (α : Type u) → (α → α → Ordering) → Type u
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.lift₂_def₂ : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6}
  (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [inst_5 : IsDirectedOrder ι] {C : Sort u_9}
  (ih : (i : ι) → F₁ i → F₂ i → C)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (x : (i : ι) × F₁ i) (y : (i : ι) × F₂ i) (i : ι) (hxi : x.fst ≤ i) (hyi : y.fst ≤ i),
  DirectLimit.lift₂ f₁ f₂ ih compat ⟦x⟧ ⟦y⟧ = ih i ((f₁ x.fst i hxi) x.snd) ((f₂ y.fst i hyi) y.snd)
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.toList.match_1.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (i : ι) (x : M i) (a : x ≠ 1)
  (h_1 : (i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a))
  (h_2 :
    (x x_1 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord M x j) →
        (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_1) → motive x x_1 (w₁.append _hne w₂)),
  (match i, i, Monoid.CoprodI.NeWord.singleton x a with
    | i, .(i), Monoid.CoprodI.NeWord.singleton x a => h_1 i x a
    | x, x_1, w₁.append _hne w₂ => h_2 x x_1 j k w₁ _hne w₂) =
    h_1 i x a
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.tryRecv : {α : Type} → Std.CloseableChannel.Bounded✝ α → BaseIO (Option α)
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.baseId : Lean.Elab.FVarAliasInfo → Lean.FVarId
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instCoeSortSkeleton : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] → (α : Sort u_2) → [CoeSort C α] → CoeSort (CategoryTheory.Skeleton C) α
-- Init.Data.AC
Lean.Data.AC.Context.eq_of_norm : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (a b : Lean.Data.AC.Expr),
  (Lean.Data.AC.norm ctx a == Lean.Data.AC.norm ctx b) = true → Lean.Data.AC.eval α ctx a = Lean.Data.AC.eval α ctx b
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addLeftCancelMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁]
  [inst_3 : AddLeftCancelMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addLeftCancelMonoid f hf one mul npow =
    { toAddMonoid := Function.Injective.addMonoid f hf one mul npow, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.rightUniformSpace_eq : ∀ {G : Type u_2} [u : UniformSpace G] [inst : Group G] [inst_1 : IsUniformGroup G],
  IsTopologicalGroup.rightUniformSpace G = u
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.Cauchy.instNonTrivial : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [Nontrivial β],
  Nontrivial (CauSeq.Completion.Cauchy abv)
-- Init.Prelude
instOfNatNat : (n : ℕ) → OfNat ℕ n
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.locallyOfFiniteType_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.LocallyOfFiniteType f]
  [hg : AlgebraicGeometry.LocallyOfFiniteType g],
  AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.Rel
Function.graph_id : ∀ {α : Type u_1}, Function.graph id = SetRel.id
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.splitter : (motive : Lean.Expr → Sort u_1) →
  (e : Lean.Expr) →
    ((a : Lean.Literal) → motive (Lean.Expr.lit a)) →
      ((mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId)) →
        ((deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex)) →
          ((fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId)) →
            ((declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us)) →
              ((u : Lean.Level) → motive (Lean.Expr.sort u)) →
                ((e : Lean.Expr) →
                    (∀ (a : Lean.Literal), e = Lean.Expr.lit a → False) →
                      (∀ (mvarId : Lean.MVarId), e = Lean.Expr.mvar mvarId → False) →
                        (∀ (deBruijnIndex : ℕ), e = Lean.Expr.bvar deBruijnIndex → False) →
                          (∀ (fvarId : Lean.FVarId), e = Lean.Expr.fvar fvarId → False) →
                            (∀ (declName : Lean.Name) (us : List Lean.Level), e = Lean.Expr.const declName us → False) →
                              (∀ (u : Lean.Level), e = Lean.Expr.sort u → False) → motive e) →
                  motive e
-- Init.Data.BitVec.Lemmas
BitVec.shiftLeft_and_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x &&& y) <<< n = x <<< n &&& y <<< n
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.isSymmetric_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} {T : ι → E →ₗ[𝕜] E} (s : Finset ι), (∀ i ∈ s, (T i).IsSymmetric) → (∑ i ∈ s, T i).IsSymmetric
-- Mathlib.Algebra.Squarefree.Basic
/-- `x * y` is square-free iff `x` and `y` have no common factors and are themselves square-free.  -/
squarefree_mul_iff : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y : R} [DecompositionMonoid R],
  Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the denominator of a right fraction  -/
CategoryTheory.MorphismProperty.RightFraction.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.RightFraction X Y) → self.X' ⟶ X
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.coeff_toPowerSeries_symm : ∀ {R : Type u_2} [inst : Semiring R] {f : PowerSeries R} {n : ℕ},
  (HahnSeries.toPowerSeries.symm f).coeff n = (PowerSeries.coeff n) f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.strictAntiOn_node : ∀ (n : ℕ), StrictAntiOn (fun x => Polynomial.Chebyshev.node n x) ↑(Finset.range (n + 1))
-- Mathlib.Order.NonemptyFiniteChains
/-- a finite subset  -/
PartialOrder.NonemptyFiniteChains.finset : {X : Type u} → [inst : PartialOrder X] → PartialOrder.NonemptyFiniteChains X → Finset X
-- Mathlib.Analysis.Normed.Affine.AsymptoticCone
AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [FiniteDimensional ℝ V],
  Bornology.cobounded P = ⨆ v ∈ Metric.sphere 0 1, AffineSpace.asymptoticNhds ℝ P v