mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.image.ι_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasImage 0],
  CategoryTheory.Limits.image.ι 0 = 0
-- Mathlib.Order.Max
isTop_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsTop (OrderDual.ofDual a) ↔ IsBot a
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.summable_logDeriv_one_sub_eta_q : ∀ {z : ℂ}, z ∈ UpperHalfPlane.upperHalfPlaneSet → Summable fun i => logDeriv (fun x => 1 - ModularForm.eta_q i x) z
-- Mathlib.Data.NNReal.Defs
NNReal.eq : ∀ {n m : NNReal}, ↑n = ↑m → n = m
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_smul_dvd : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} (n : ℕ), addOrderOf (n • x) ∣ addOrderOf x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Identity map as a `LinearIsometryEquiv`.  -/
LinearIsometryEquiv.refl : (R : Type u_1) →
  (E : Type u_5) → [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → E ≃ₗᵢ[R] E
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.reindexGroupEquiv_apply_simple : ∀ {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B ≃ B') (i : B'),
  (M.reindexGroupEquiv e) ((CoxeterMatrix.reindex e M).simple i) = M.simple (e.symm i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keys_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.keys = t₂.keys
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates limits, then `F.unop : C ⥤ D` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop
-- Mathlib.Tactic.DepRewrite
/-- See `visit`.  -/
Mathlib.Tactic.DepRewrite.visitInner : Lean.Expr → Option Lean.Expr → Mathlib.Tactic.DepRewrite.M Lean.Expr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β)
  (hlk_2 : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) = true),
  (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey k hlk_2 =
    match h : compare k k' with
    | Ordering.lt => l.getKey k ⋯
    | Ordering.gt => r.getKey k ⋯
    | Ordering.eq => k'
-- Mathlib.RingTheory.Norm.Basic
Algebra.prod_embeddings_eq_finrank_pow : ∀ {K : Type u_4} {L : Type u_5} (F : Type u_6) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F]
  [inst_3 : Algebra K L] [inst_4 : Algebra K F] (E : Type u_7) [inst_5 : Field E] [inst_6 : Algebra K E]
  [inst_7 : Algebra L F] [IsScalarTower K L F] [IsAlgClosed E] [Algebra.IsSeparable K F]
  [inst_11 : FiniteDimensional K F] (pb : PowerBasis K L),
  ∏ σ, σ ((algebraMap L F) pb.gen) = (∏ σ, σ pb.gen) ^ Module.finrank L F
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A countable sum of finite measures is s-finite.
This lemma is superseded by the instance below.  -/
MeasureTheory.sfinite_sum_of_countable : ∀ {α : Type u_1} {ι : Type u_3} {m0 : MeasurableSpace α} [Countable ι] (m : ι → MeasureTheory.Measure α)
  [∀ (n : ι), MeasureTheory.IsFiniteMeasure (m n)], MeasureTheory.SFinite (MeasureTheory.Measure.sum m)
-- Mathlib.Topology.Inseparable
Inseparable.map_of_continuousOn : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y}
  {s : Set X}, Inseparable x y → ContinuousOn f s → x ∈ s → y ∈ s → Inseparable (f x) (f y)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.splitSource : Lean.Meta.Grind.SplitDiagInfo → Lean.Meta.Grind.SplitSource
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.instAddAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  AddOpposite.instAddAction = { toVAdd := AddOpposite.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Algebra.Category.Ring.FilteredColimits
SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget₂ SemiRingCat MonCat)
-- Init.Meta.Defs
Lean.Meta.Occurrences.contains : Lean.Meta.Occurrences → ℕ → Bool
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheck.mk.injEq : ∀ (site : Lean.Doc.DeferredCheckSite) (index : ℕ) (sourceString : String) (imports : Array Lean.Name)
  (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (options : Lean.Options) (check : Dynamic)
  (site_1 : Lean.Doc.DeferredCheckSite) (index_1 : ℕ) (sourceString_1 : String) (imports_1 : Array Lean.Name)
  (currNamespace_1 : Lean.Name) (openDecls_1 : List Lean.OpenDecl) (options_1 : Lean.Options) (check_1 : Dynamic),
  ({ site := site, index := index, sourceString := sourceString, imports := imports, currNamespace := currNamespace,
        openDecls := openDecls, options := options, check := check } =
      { site := site_1, index := index_1, sourceString := sourceString_1, imports := imports_1,
        currNamespace := currNamespace_1, openDecls := openDecls_1, options := options_1, check := check_1 }) =
    (site = site_1 ∧
      index = index_1 ∧
        sourceString = sourceString_1 ∧
          imports = imports_1 ∧
            currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ options = options_1 ∧ check = check_1)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_univ : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β}, e.restr Set.univ = e
-- Mathlib.Algebra.FreeAlgebra
/-- One in `Pre R X` defined as the image of `1` from `R`. Note: Used for notation only.  -/
FreeAlgebra.Pre.hasOne : (R : Type u_1) → (X : Type u_2) → [CommSemiring R] → One (FreeAlgebra.Pre R X)
-- Mathlib.Data.Finset.Defs
Finset.decidableDforallFinset : {α : Type u_1} →
  {s : Finset α} →
    {p : (a : α) → a ∈ s → Prop} →
      [_hp : (a : α) → (h : a ∈ s) → Decidable (p a h)] → Decidable (∀ (a : α) (h : a ∈ s), p a h)
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The type of morphisms in `TopRep k G`.  -/
TopRep.Hom : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : Ring k] → [inst_2 : Monoid G] → TopRep k G → TopRep k G → Type (max u_1 u_2)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instNegCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Neg (CauSeq.Completion.Cauchy abv)
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) (v : ι → M), e.det v = (e.toMatrix v).det
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.fst_prod : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset (M × N)),
  s.prod.1 = (Multiset.map Prod.fst s).prod
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- A non-empty set with no doubling is the left-translate of its stabilizer.  -/
Finset.vadd_stabilizer_of_no_doubling : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  (A + A).card ≤ A.card → a ∈ A → a +ᵥ ↑(AddAction.stabilizer G A) = ↑A
-- Mathlib.Logic.Equiv.Set
/-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`.  -/
Equiv.Set.sep : {α : Type u} → (s : Set α) → (t : α → Prop) → ↑{x | x ∈ s ∧ t x} ≃ ↑{x | t ↑x}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → (Std.TreeMap.Raw.ofList l cmp)[k']? = some v
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isOpen_iff_scottContinuous_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : TopologicalSpace α] [Topology.IsScott α Set.univ],
  IsOpen s ↔ ScottContinuous fun x => x ∈ s
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instT2Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [T2Space R], T2Space (ContinuousMapZero X R)
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle_injective : ∀ (N : ℕ) [inst : NeZero N], Function.Injective ⇑ZMod.toAddCircle
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMonoidWithZero : {α : Type u_1} →
  [DecidableEq α] → [inst : MonoidWithZero α] → [NoZeroDivisors α] → [Nontrivial α] → MonoidWithZero (WithBot α)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instSMulNat : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → SMul ℕ (ArchimedeanClass R)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
ContinuousLinearMap.map_tsum : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
  {L : SummationFilter ι} [T2Space M₂] [L.NeBot] {f : ι → M} (φ : M →SL[σ] M₂),
  Summable f L → φ (∑'[L] (z : ι), f z) = ∑'[L] (z : ι), φ (f z)
-- Mathlib.Algebra.Group.AddChar
AddChar.compAddMonoidHom_apply : ∀ {A : Type u_1} {B : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : Monoid M]
  (ψ : AddChar B M) (f : A →+ B) (a : A), (ψ.compAddMonoidHom f) a = ψ (f a)
-- Mathlib.Topology.ContinuousMap.Interval
/-- The map `projIcc` from `α` onto an interval in `α`, as a `ContinuousMap`.  -/
ContinuousMap.projIccCM : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] → [OrderTopology α] → {a b : α} → [Fact (a ≤ b)] → C(α, ↑(Set.Icc a b))
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.growsPolynomially_const : ∀ {c : ℝ}, AkraBazziRecurrence.GrowsPolynomially fun x => c
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inf_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] (s t : Finset α) (f : α → β), (s * t).inf f = s.inf fun x => t.inf fun x_1 => f (x * x_1)
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- `Pi.monoidalCategory C` equips the product of an indexed family of categories with
the pointwise monoidal structure.  -/
CategoryTheory.Pi.monoidalCategory : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [(i : I) → CategoryTheory.MonoidalCategory (C i)] → CategoryTheory.MonoidalCategory ((i : I) → C i)
-- Mathlib.Data.Set.MemPartition
/-- `memPartition f n` is the partition containing at most `2^(n+1)` sets, where each set contains
the points that for all `i` belong to one of `f i` or its complement.  -/
memPartition : {α : Type u_1} → (ℕ → Set α) → ℕ → Set (Set α)
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁ : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E : Type u₅} [inst_2 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [inst_3 : W₂.ContainsIdentities],
  W₁.Q.comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF) =
    CategoryTheory.Functor.curry.obj F
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- In a preadditive category, if the coproduct over `f : J → C` exists,
then the biproduct over `f` exists.  -/
CategoryTheory.Limits.HasBiproduct.of_hasCoproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_1}
  [Finite J] (f : J → C) [CategoryTheory.Limits.HasCoproduct f], CategoryTheory.Limits.HasBiproduct f
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousAt.rpow : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ℝ} {x : α},
  ContinuousAt f x → ContinuousAt g x → f x ≠ 0 ∨ 0 < g x → ContinuousAt (fun t => f t ^ g t) x
-- Mathlib.Topology.Filter
Filter.closure_singleton : ∀ {α : Type u_2} (l : Filter α), closure {l} = Set.Ici l
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.containsThenInsert_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.containsThenInsert k).1 = t.contains k
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulLeftMono_of_mulLeftStrictMono : ∀ (M : Type u_3) [inst : Mul M] [inst_1 : PartialOrder M] [MulLeftStrictMono M], MulLeftMono M
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.mk.injEq : ∀ (leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (leadingParsers : List (Lean.Parser.Parser × ℕ))
  (trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (trailingParsers : List (Lean.Parser.Parser × ℕ))
  (leadingTable_1 : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (leadingParsers_1 : List (Lean.Parser.Parser × ℕ))
  (trailingTable_1 : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)) (trailingParsers_1 : List (Lean.Parser.Parser × ℕ)),
  ({ leadingTable := leadingTable, leadingParsers := leadingParsers, trailingTable := trailingTable,
        trailingParsers := trailingParsers } =
      { leadingTable := leadingTable_1, leadingParsers := leadingParsers_1, trailingTable := trailingTable_1,
        trailingParsers := trailingParsers_1 }) =
    (leadingTable = leadingTable_1 ∧
      leadingParsers = leadingParsers_1 ∧ trailingTable = trailingTable_1 ∧ trailingParsers = trailingParsers_1)
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- Given a symmetric generating set of a permutation group, if T is a nonempty proper subset of
an orbit, then there exists a generator that sends some element of T into the complement of T.  -/
exists_smul_notMem_of_subset_orbit_closure : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (S : Set G) (T : Set α) {a : α},
  (∀ g ∈ S, g⁻¹ ∈ S) → T ⊆ MulAction.orbit (↥(Subgroup.closure S)) a → a ∉ T → T.Nonempty → ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
-- Lean.Elab.Tactic.RCases
/-- Takes a list of constructor names, and an (alternation) list of patterns, and matches each
pattern against its constructor. It returns the list of names that will be passed to `cases`,
and the list of `(constructor name, patterns)` for each constructor, where `patterns` is the
(conjunctive) list of patterns to apply to each constructor argument.
 -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructors : Lean.Syntax →
  ℕ →
    optParam (Array Lean.Meta.AltVarNames) #[] →
      List Lean.Name →
        List Lean.Elab.Tactic.RCases.RCasesPatt →
          Lean.MetaM (Array Lean.Meta.AltVarNames × List (Lean.Name × List Lean.Elab.Tactic.RCases.RCasesPatt))
-- Mathlib.Data.List.AList
AList.lookup_union_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : AList β},
  AList.lookup a (s₁ ∪ s₂) = some b ↔ AList.lookup a s₁ = some b ∨ a ∉ s₁ ∧ AList.lookup a s₂ = some b
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatIso_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] [inst_5 : RF'.IsRightDerivedFunctor α' W] (τ : F ≅ F'),
  (RF.rightDerivedNatIso RF' α α' W τ).hom = RF.rightDerivedNatTrans RF' α α' W τ.hom
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.unusedAltIdxs : Lean.Meta.Match.MatcherResult → List ℕ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceBNe : Lean.Meta.Simp.DSimproc
-- Init.MetaTypes
Lean.NameGenerator.mk.injEq : ∀ (namePrefix : Lean.Name) (idx : ℕ) (namePrefix_1 : Lean.Name) (idx_1 : ℕ),
  ({ namePrefix := namePrefix, idx := idx } = { namePrefix := namePrefix_1, idx := idx_1 }) =
    (namePrefix = namePrefix_1 ∧ idx = idx_1)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- If `pp.tagAppFns` is set, and if the current expression is a constant application,
then `d` is evaluated with the head constant delaborated with `delabConst` as the ref.
 -/
Lean.PrettyPrinter.Delaborator.withFnRefWhenTagAppFns : Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_add : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SWOT[σ] F}, (f + g).toCLM = f.toCLM + g.toCLM
-- Mathlib.Order.Bounded
Set.bounded_ge_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 ≥ x2) (Set.Ici a)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableAt.cpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {c : ℂ},
  DifferentiableAt ℂ f x → f x ∈ Complex.slitPlane → DifferentiableAt ℂ (fun x => f x ^ c) x
-- Mathlib.Order.Filter.Basic
Filter.eventually_mem_set : ∀ {α : Type u} {s : Set α} {l : Filter α}, (∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Bounded.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Ordnode.nil.Bounded (some a) (some b) = (a < b)
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_mono_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : UpperSet α} {t : UpperSet β},
  s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
-- Init.Data.BitVec.Lemmas
BitVec.zero_srem : ∀ {w : ℕ} {x : BitVec w}, (0#w).srem x = 0#w
-- Init.Core
UInt32.ofBitVec.injEq : ∀ (toBitVec toBitVec_1 : BitVec 32), ({ toBitVec := toBitVec } = { toBitVec := toBitVec_1 }) = (toBitVec = toBitVec_1)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- Show there are finitely many partitions by considering the surjection from compositions to
partitions.
 -/
Nat.Partition.instFintype : (n : ℕ) → Fintype n.Partition
-- Mathlib.Order.Birkhoff
UpperSet.infIrred_Ici : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), InfIrred (UpperSet.Ici a)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.inertiaDegIn_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B] [Module.Finite A B]
  [FaithfulSMul A B] {p : Ideal A} [p.IsPrime], p.inertiaDegIn B ≠ 0
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i)
      (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) (K.iCycles j)) =
    K.d i j
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
CategoryTheory.ObjectProperty.localEpi_mem_range_iff_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [G.Faithful] [G.Full] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.ObjectProperty.localEpi (fun x => x ∈ Set.range G.obj) f ↔ CategoryTheory.Epi (F.map f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.go.eq_2 : ∀ (k k_1 : ℤ) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst.go k (Lean.Grind.CommRing.Poly.add k_1 m p_1) =
    Lean.Grind.CommRing.Poly.add (k * k_1) m (Lean.Grind.CommRing.Poly.mulConst.go k p_1)
-- Mathlib.Data.List.Rotate
List.rotate.eq_1 : ∀ {α : Type u_1} (l : List α) (n : ℕ),
  l.rotate n =
    match List.splitAt (n % l.length) l with
    | (l₁, l₂) => l₂ ++ l₁
-- Init.Grind.ToIntLemmas
_private.Init.Grind.ToIntLemmas.0.Lean.Grind.ToInt.isNonempty : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [Lean.Grind.ToInt α i] (a : α), i.nonEmpty = true
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_unique : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : Unique α] (f : α → ENNReal),
  ∫⁻ (x : α), f x ∂μ = f default * μ Set.univ
-- Init.Data.Option.Basic
/-- Converts an optional value to an array with zero or one element.

Examples:
* `(some "value").toArray = #["value"]`
* `none.toArray = #[]`
 -/
Option.toArray : {α : Type u_1} → Option α → Array α
-- Mathlib.Data.Sigma.Basic
Sigma.curry_uncurry : ∀ {α : Type u_1} {β : α → Type u_4} {γ : (a : α) → β a → Type u_7} (f : (x : α) → (y : β x) → γ x y),
  Sigma.curry (Sigma.uncurry f) = f
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_add_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ∀ (n : ℕ) [inst_4 : n.AtLeastTwo], ⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- Consider a pullback square of types where the right map is a monomorphism.
If the right and bottom map are jointly surjective, and the bottom map
is injective on the complement on the range of the left map, then the square
is a pushout square.  -/
CategoryTheory.Limits.Types.isPushout_of_isPullback_of_mono' : ∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPullback t l r b →
    ∀ [CategoryTheory.Mono r],
      Set.range ⇑(CategoryTheory.ConcreteCategory.hom r) ⊔ Set.range ⇑(CategoryTheory.ConcreteCategory.hom b) =
          Set.univ →
        (∀ (x₃ y₃ : X₃),
            x₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
              y₃ ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom l) →
                (CategoryTheory.ConcreteCategory.hom b) x₃ = (CategoryTheory.ConcreteCategory.hom b) y₃ → x₃ = y₃) →
          CategoryTheory.IsPushout t l r b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.coe_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [Nonempty ι] [inst_2 : InfSet α] {f : ι → α},
  BddBelow (Set.range f) → ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Lean.Elab.InfoTree.Basic
Lean.Elab.Info.toElabInfo? : Lean.Elab.Info → Option Lean.Elab.ElabInfo
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.objMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {f g : CategoryTheory.Arrow C} (φ : f ⟶ g),
  CategoryTheory.SmallObject.objMap I κ φ =
    CategoryTheory.Arrow.Hom.left ((CategoryTheory.SmallObject.iteration I κ).map φ)