mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesRightHomologyOf.mk : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D}
  [inst_4 : F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C},
  (∀ (h : S.RightHomologyData), h.IsPreservedBy F) → F.PreservesRightHomologyOf S
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.param_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β],
  Asymptotics.SuperpolynomialDecay l k f → Asymptotics.SuperpolynomialDecay l k (k * f)
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.finite_of_epi : ∀ {X Y : SSet} [X.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Epi f], Y.Finite
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
CategoryTheory.instPreservesFiniteProductsFunctorColimOfPreadditive : ∀ {A : Type u_1} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} J] [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J A]
  [CategoryTheory.Preadditive A], CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `σₘ[A]` of a finset `A` in a group is `|A / A| / |A|`.  -/
Combinatorics.Additive.«termδₘ[_]» : Lean.ParserDescr
-- Lean.Meta.Sym.Apply
/-- Creates a value to assign to input goal metavariable using unification result.

Handles both constant expressions (common case, avoids `instantiateLevelParams`)
and general expressions.
 -/
_private.Lean.Meta.Sym.Apply.0.Lean.Meta.Sym.mkValue : Lean.Expr → Lean.Meta.Sym.Pattern → Lean.Meta.Sym.MatchUnifyResult → Lean.Expr
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instConcreteCategoryContinuousHomCarrier : CategoryTheory.ConcreteCategory ωCPO fun x1 x2 => x1.carrier →𝒄 x2.carrier
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_ulift : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R (ULift.{w, v} M) = Cardinal.lift.{w, v} (Module.rank R M)
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_iff_comp_add_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (x + b)) (a - b)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The kernel built from `kernel.ι f` is limiting.  -/
CategoryTheory.Limits.kernelIsKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.kernel.ι f) ⋯)
-- Init.Data.Array.Attach
Array.filterMap_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β},
  Array.filterMap f (wfParam xs) = Array.filterMap f xs.attach.unattach
-- Init.Data.List.Find
List.idxOf?_eq_map_finIdxOf?_val : ∀ {α : Type u_1} [inst : BEq α] {xs : List α} {a : α}, List.idxOf? a xs = Option.map (fun x => ↑x) (List.finIdxOf? a xs)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithLower α)
-- Init.Omega.Constraint
/-- The coefficients of the new equation generated when solving a hard equality.  -/
Lean.Omega.bmod_coeffs : ℕ → ℕ → Lean.Omega.Coeffs → Lean.Omega.Coeffs
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`
(as explicit arguments).  -/
CategoryTheory.Limits.IsInitial.ofUniqueHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (h : (Y : C) → X ⟶ Y) → (∀ (Y : C) (m : X ⟶ Y), m = h Y) → CategoryTheory.Limits.IsInitial X
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `elemExponent_min` using `ExpChar`.  -/
IsPurelyInseparable.elemExponent_min' : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (p : ℕ) [ExpChar K p] {a : L} {n : ℕ},
  n < IsPurelyInseparable.elemExponent K a → a ^ p ^ n ∉ (algebraMap K L).range
-- Mathlib.CategoryTheory.Products.Basic
/-- `F.flip` composed with evaluation is the same as evaluating `F`.  -/
CategoryTheory.flipCompEvaluation : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) →
              (a : A) → F.flip.comp ((CategoryTheory.evaluation A C).obj a) ≅ F.obj a
-- Mathlib.GroupTheory.Nilpotent
/-- Abelian groups are nilpotent.  -/
AddCommGroup.isNilpotent : ∀ {G : Type u_2} [inst : AddCommGroup G], AddGroup.IsNilpotent G
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with addition.  -/
ContDiffAt.laplacianWithin_add_nhdsWithin : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E},
  ContDiffWithinAt ℝ 2 f₁ s x →
    ContDiffWithinAt ℝ 2 f₂ s x →
      UniqueDiffOn ℝ s →
        x ∈ s →
          InnerProductSpace.laplacianWithin (f₁ + f₂) s =ᶠ[nhdsWithin x s]
            InnerProductSpace.laplacianWithin f₁ s + InnerProductSpace.laplacianWithin f₂ s
-- Mathlib.Algebra.DualNumber
DualNumber.range_inlAlgHom_sup_adjoin_eps : ∀ {R : Type u_1} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (TrivSqZeroExt.inlAlgHom R A A).range ⊔ R[DualNumber.eps] = ⊤
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.finset_inf_arrow_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {I : Type u_1} {B : C} (s : Finset I) (P : I → CategoryTheory.Subobject B), ∀ i ∈ s, (P i).Factors (s.inf P).arrow
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_rco : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((compare e lowerBound).isGE = true ∧ (compare e upperBound).isLT = true)) t.keys
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The sum of the sizes of the blocks in a composition up to `i`.  -/
Composition.sizeUpTo : {n : ℕ} → Composition n → ℕ → ℕ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.core : Lean.Expr →
  Lean.Expr →
    Lean.Meta.Grind.Arith.CommRing.RingExpr →
      Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z) h)
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- The obvious bijection between `Πʳ i, [R i, A i]_[⊤]` and `Π i, A i` is a homeomorphism.  -/
RestrictedProduct.homeoTop : {ι : Type u_1} →
  {R : ι → Type u_2} →
    {A : (i : ι) → Set (R i)} →
      [inst : (i : ι) → TopologicalSpace (R i)] →
        ((i : ι) → ↑(A i)) ≃ₜ RestrictedProduct (fun i => R i) (fun i => A i) ⊤
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.body.inj : ∀ {name : Lean.Name} {next : Mathlib.Tactic.Conv.Path} {name_1 : Lean.Name} {next_1 : Mathlib.Tactic.Conv.Path},
  Mathlib.Tactic.Conv.Path.body name next = Mathlib.Tactic.Conv.Path.body name_1 next_1 → name = name_1 ∧ next = next_1
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R) {Z : PresheafOfModules R} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp M.toFreeYonedaCoproduct
      (CategoryTheory.CategoryStruct.comp M.fromFreeYonedaCoproduct h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfHomEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : CategoryTheory.Adjunction.CoreHomEquiv F G),
  CategoryTheory.Adjunction.mkOfHomEquiv adj =
    CategoryTheory.Adjunction.mk'
      { homEquiv := adj.homEquiv,
        unit :=
          { app := fun X => (adj.homEquiv X (F.obj X)) (CategoryTheory.CategoryStruct.id (F.obj X)), naturality := ⋯ },
        counit :=
          {
            app := fun Y =>
              (adj.homEquiv (G.obj Y) ((CategoryTheory.Functor.id D).obj Y)).invFun
                (CategoryTheory.CategoryStruct.id (G.obj Y)),
            naturality := ⋯ },
        homEquiv_unit := ⋯, homEquiv_counit := ⋯ }
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_some_iff : ∀ {s : String.Slice} {a : ℤ},
  s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = ↑b) ∨ ∃ t, s.copy = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -↑b
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
_private.Mathlib.NumberTheory.Harmonic.GammaDeriv.0.Complex.HasDerivAt.complex_of_real : ∀ {f : ℂ → ℂ} {g : ℝ → ℝ} {g' s : ℝ},
  DifferentiableAt ℂ f ↑s → HasDerivAt g g' s → (∀ (s : ℝ), f ↑s = ↑(g s)) → HasDerivAt f ↑g' ↑s
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_vadd_inter_vadd : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x y : G),
  ((x +ᵥ A) ∩ (y +ᵥ B)).card = A.addConvolution (-B) (-x + y)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.const_sub : ∀ {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 → ∀ (c : F), InnerProductSpace.HarmonicContOnCl ((fun x => c) - f) s
-- Mathlib.Data.Part
Part.union_mem_union : ∀ {α : Type u_1} [inst : Union α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma ∪ mb ∈ a ∪ b
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.tail_cons : ∀ {α : Type u_1} {n : ℕ} (x : Fin n ↪ α) {a : α} (ha : a ∉ Set.range ⇑x),
  Fin.Embedding.tail (Fin.Embedding.cons x ha) = x
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_pow : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  PowerSeries.HasSubst a → ∀ (f : PowerSeries R) (n : ℕ), PowerSeries.subst a (f ^ n) = PowerSeries.subst a f ^ n
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimitsOfShape.of_small : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfSize.{v₁, u₁, v, u} C]
  (J : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} J] [Small.{u₁, u₂} J]
  [CategoryTheory.LocallySmall.{v₁, v₂, u₂} J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_prod_le : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.num.inj : ∀ {v v_1 : ℤ}, Int.Internal.Linear.Expr.num v = Int.Internal.Linear.Expr.num v_1 → v = v_1
-- Init.SimpLemmas
and_assoc : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c
-- Init.System.IO
/-- Executes arbitrary side effects in a pure context, with exceptions indicated via `Except`. This a
**dangerous** operation that can easily undermine important assumptions about the meaning of Lean
programs, and it should only be used with great care and a thorough understanding of compiler
internals, and even then only to implement observationally pure operations.

This function is not a good way to convert an `EIO α` or `IO α` into an `α`. Instead, use
[`do`-notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation).

Because the resulting value is treated as a side-effect-free term, the compiler may re-order,
duplicate, or delete calls to this function. The side effect may even be hoisted into a constant,
causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
unsafeEIO : {ε α : Type} → EIO ε α → Except ε α
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.case.inj : ∀ {a a_1 a_2 a_3 : Turing.ToPartrec.Code}, a.case a_1 = a_2.case a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.weakEquivalence_resolutionMap_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap f) ↔
    HomotopicalAlgebra.WeakEquivalence f
-- Init.Data.Order.Classes
Std.MaxEqOr.mk : ∀ {α : Type u} [inst : Max α], (∀ (a b : α), a ⊔ b = a ∨ a ⊔ b = b) → Std.MaxEqOr α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp), t = t_1 → ∀ (a : α), t.get? a = t_1.get? a
-- Mathlib.Analysis.Normed.Lp.LpEquiv
equiv_lpPiLp_norm : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Fintype α]
  (f : ↥(lp E p)), ‖Equiv.lpPiLp f‖ = ‖f‖
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.insert a b)).buckets).Perm
        (Std.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.inv_toFun : ∀ {t : Tactic.ComputeAsymptotics.Monomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → t.inv.toFun basis =ᶠ[Filter.atTop] (t.toFun basis)⁻¹
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₂.eq_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'')
  (n : ℕ),
  Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ n.succ =
    ⟨CategoryTheory.CategoryStruct.comp (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).fst
        (HomologicalComplex.xPrevIso Q ⋯).inv,
      ⟨CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ⋯).hom
          (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).snd.fst,
        ⋯⟩⟩
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.trivial_grp_inv : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the right by a function preserves uniform Cauchy sequences  -/
UniformCauchySeqOn.comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
  {γ : Type u_5}, UniformCauchySeqOn F p s → ∀ (g : γ → α), UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.mkContinuousMultilinear_norm_le : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} {G : Type wG} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G]
  [inst_6 : Fintype ι] [inst_7 : (i : ι') → SeminormedAddCommGroup (E' i)] [inst_8 : (i : ι') → NormedSpace 𝕜 (E' i)]
  (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ},
  0 ≤ C →
    ∀ (H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖),
      ‖f.mkContinuousMultilinear C H‖ ≤ C
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_toList_rcc : ∀ {m n : ℤ}, (m...=n).toList.toArray = (m...=n).toArray
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsElliptic.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] (m : Matrix (Fin 2) (Fin 2) R), m.IsElliptic = (m.discr < 0)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (i : ℕ),
  ModuleCat.Hom.hom ((groupCohomology.cochainsMap f φ).f i) =
    (Rep.Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x => ⇑f ∘ x
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.instUniqueOfIsEmpty : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {H : SimpleGraph W} → [IsEmpty V] → Unique (G →g H)
-- Mathlib.Analysis.InnerProductSpace.Defs
_private.Mathlib.Analysis.InnerProductSpace.Defs.0.InnerProductSpace.Core.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_eq_self_of_norm_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {x : V}, ‖x‖ = 1 → NormedSpace.normalize x = x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.exprToRingId : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.Dynamics.Ergodic.Ergodic
Ergodic.symm_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α},
  Ergodic (⇑e.symm) μ ↔ Ergodic (⇑e) μ
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- A function which is analytic within a set is strictly differentiable there. Since we
don't have a predicate `HasStrictFDerivWithinAt`, we spell out what it would mean.  -/
HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinAt f p s x →
    (fun y =>
        f y.1 - f y.2 -
          ((continuousMultilinearCurryFin1 𝕜 E F) (p 1)) (y.1 - y.2)) =o[nhdsWithin (x, x) (insert x s ×ˢ insert x s)]
      fun y => y.1 - y.2
-- Mathlib.Data.Sum.Order
Sum.Lex.inl_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone (⇑toLex ∘ Sum.inl)
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_zero_right : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), ⁅g, 0⁆ = 0
-- Mathlib.Control.Basic
joinM_map_pure : ∀ {m : Type u → Type u} [inst : Monad m] [LawfulMonad m] {α : Type u} (a : m α), joinM (pure <$> a) = a
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_top_ne_zero : ∀ {a : ℝ}, a ≠ 0 → ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`.  -/
MeasureTheory.tendsto_setIntegral_of_L1' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : α → G),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {F : ι → α → G} {l : Filter ι},
      (∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) →
        Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F i - f) 1 μ) l (nhds 0) →
          ∀ (s : Set α), Filter.Tendsto (fun i => ∫ (x : α) in s, F i x ∂μ) l (nhds (∫ (x : α) in s, f x ∂μ))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.alternatingSum_cons_cons : ∀ {G : Type u_7} [inst : SubNegMonoid G] (a b : G) (l : List G), (a :: b :: l).alternatingSum = a - b + l.alternatingSum
-- Mathlib.LinearAlgebra.Dual.BaseChange
/-- Equivalent modules have equivalent duals.  -/
Module.Dual.congr : {R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommMonoid W] → [inst_4 : Module R W] → (V ≃ₗ[R] W) → Module.Dual R V ≃ₗ[R] Module.Dual R W
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.eq_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {a : A} {b : B}, a = e.symm b ↔ e a = b
-- Lean.Server.Requests
Lean.Server.RequestM.pureTask : {α : Type} → Lean.Server.RequestM α → Lean.Server.RequestM (Lean.Server.RequestTask α)
-- Init.Data.Ord.Basic
/-- If `a` and `b` are `Ordering`, then `a.then b` returns `a` unless it is `.eq`, in which case it
returns `b`. Additionally, it has “short-circuiting” behavior similar to boolean `&&`: if `a` is not
`.eq` then the expression for `b` is not evaluated.

This is a useful primitive for constructing lexicographic comparator functions. The `deriving Ord`
syntax on a structure uses the `Ord` instance to compare each field in order, combining the results
equivalently to `Ordering.then`.

Use `compareLex` to lexicographically combine two comparison functions.

Examples:
```lean example
structure Person where
  name : String
  age : Nat

-- Sort people first by name (in ascending order), and people with the same name by age (in
-- descending order)
instance : Ord Person where
  compare a b := (compare a.name b.name).then (compare b.age a.age)
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Dana", 50⟩
```
```output
Ordering.gt
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 50⟩
```
```output
Ordering.gt
```

```lean example
#eval Ord.compare (⟨"Gert", 33⟩ : Person) ⟨"Gert", 20⟩
```
```output
Ordering.lt
```
 -/
Ordering.then : Ordering → Ordering → Ordering