mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.Limits.IsIndObject
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.map_comp_mk : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y},
  CompactCoherentification.map f ∘ ⇑(CompactCoherentification.mk X) = ⇑(CompactCoherentification.mk Y) ∘ f
-- Mathlib.Data.Finset.Basic
Finset.filter_union_right : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] [inst_2 : DecidableEq α]
  (s : Finset α), Finset.filter p s ∪ Finset.filter q s = {x ∈ s | p x ∨ q x}
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
add_tsub_cancel_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b : α}, a ≤ b → a + (b - a) = b
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.mk : ℕ → List Lean.AsyncConst✝ → Lean.NameMap Lean.AsyncConst✝ → Lean.NameTrie Lean.AsyncConst✝ → Lean.AsyncConsts✝
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_sub : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ₁ φ₂ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (φ₁ - φ₂) = TopModuleCat.Hom.hom φ₁ - TopModuleCat.Hom.hom φ₂
-- Init.Data.Dyadic.Basic
Dyadic.roundUp.eq_1 : ∀ (prec : ℤ), Dyadic.zero.roundUp prec = Dyadic.zero
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- `X` is initial if the cocone it induces on the empty diagram is colimiting.  -/
CategoryTheory.Limits.IsInitial : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max (max 0 u₁) v₁)
-- Mathlib.RingTheory.RingInvo
RingInvo.map_eq_zero_iff : ∀ {R : Type u_2} [inst : Semiring R] (f : RingInvo R) {x : R}, f x = 0 ↔ x = 0
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'.eq_1 : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (P : Ideal S),
  p.inertiaDeg' P = if hPp : Ideal.comap (algebraMap R S) P = p then Module.finrank (R ⧸ p) (S ⧸ P) else 0
-- Lean.Hygiene
_private.Lean.Hygiene.0.Lean.mkFreshInaccessibleUserName : Lean.Name → ℕ → StateM Lean.NameSanitizerState Lean.Name
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk : {R : Type u} → {a b : R} → R → R → QuadraticAlgebra R a b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G] {X' Y' : D}
  (f' g' : X' ⟶ Y') [inst_5 : CategoryTheory.Limits.HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y')
  (wf : CategoryTheory.CategoryStruct.comp (G.map f) q = CategoryTheory.CategoryStruct.comp p f')
  (wg : CategoryTheory.CategoryStruct.comp (G.map g) q = CategoryTheory.CategoryStruct.comp p g') {Z' : D} (h : Y' ⟶ Z')
  (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.coequalizer.π f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (G.map f) (G.map g) f' g' p q wf wg))
          (CategoryTheory.Limits.coequalizer.desc h wh))) =
    CategoryTheory.CategoryStruct.comp q h
-- Mathlib.Order.Hom.WithTopBot
WithTop.coeOrderHom.eq_1 : ∀ {α : Type u_4} [inst : Preorder α], WithTop.coeOrderHom = { toFun := WithTop.some, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.instInhabitedRelevantArg : Inhabited Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Algebra.Group.Commute.Units
Units.val_inv_ofPowEqOne : ∀ {M : Type u_1} [inst : Monoid M] (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0),
  ↑(Units.ofPowEqOne a n ha hn)⁻¹ = a ^ (n - 1)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- The "base" of `v` relative to a morphism `f`.

In the case that `v` is the set of roots of a crystallographic root system, and `S = ℚ`, this is the
base of the root system associated to `f`.  -/
IsAddIndecomposable.baseOf : {ι : Type u_1} →
  {M : Type u_2} →
    {S : Type u_4} → [inst : AddMonoid M] → [LinearOrder S] → [inst_2 : AddMonoid S] → (ι → M) → (M →+ S) → Set ι
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.comp_factorThru : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J X Y : C} [inst_1 : CategoryTheory.Injective J]
  (g : X ⟶ J) (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Injective.factorThru g f) = g
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_of_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {k : ι}, P.root k = P.root j + P.root i → RootPairing.chainBotCoeff i k = RootPairing.chainBotCoeff i j + 1
-- Init.Data.List.Attach
List.count_attach : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : { x // x ∈ l }}, List.count a l.attach = List.count (↑a) l
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_ofSubsingleton_id : ∀ (𝕜 : Type u) {ι : Type v} (G : Type wG) [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace 𝕜 G] [inst_4 : Subsingleton ι] [Nontrivial G] (i : ι),
  ‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ = 1
-- Mathlib.Logic.Function.Basic
Bool.involutive_not : Function.Involutive not
-- Mathlib.Data.Set.Finite.Lattice
Finite.Set.finite_biUnion : ∀ {α : Type u} {ι : Type u_1} (s : Set ι) [Finite ↑s] (t : ι → Set α), (∀ i ∈ s, Finite ↑(t i)) → Finite ↑(⋃ x ∈ s, t x)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.instIsIsoDescι : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f],
  CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun a => CategoryTheory.Limits.Sigma.ι f a)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_iSup : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Sort u_2} {f : ι → AddSubgroup (AddUnits M)},
  (iSup f).ofAddUnits = ⨆ i, (f i).ofAddUnits
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.quotientFunc.congr_simp : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k k_1 : ℤ} (e_k : k = k_1) [inst_1 : SlashInvariantFormClass F 𝒢 k]
      (q q_1 : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
      q = q_1 →
        ∀ (τ τ_1 : UpperHalfPlane),
          τ = τ_1 → SlashInvariantForm.quotientFunc f q τ = SlashInvariantForm.quotientFunc f_1 q_1 τ_1
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.completeOn_edgeSet : ∀ {α : Type u_1} (f : Set α), (Hypergraph.completeOn f).edgeSet = 𝒫 f
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.prec.inj : ∀ {a a_1 a_2 a_3 : Nat.Partrec.Code}, a.prec a_1 = a_2.prec a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.Set.Card
Set.Finite.injOn_of_encard_image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, s.Finite → (f '' s).encard = s.encard → Set.InjOn f s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.attrs : Lean.Elab.Term.LetRecToLift → Array Lean.Elab.Attribute
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_obj_right_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T)),
  ((CategoryTheory.StructuredArrow.ofDiagEquivalence.functor X).obj Y).right.right = Y.right
-- Mathlib.Computability.Primrec.List
Primrec.listLookup : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : DecidableEq α],
  Primrec₂ List.lookup
-- Mathlib.Order.Interval.Basic
Interval.subset_coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α →o β) (s : Interval α),
  ⇑f '' ↑s ⊆ ↑(Interval.map f s)
-- Mathlib.Analysis.Complex.Hadamard
/-- **Hadamard three-line theorem** on `re ⁻¹' [0, 1]` (Variant in simpler terms): Let `f` be a
bounded function, continuous on the closed strip `re ⁻¹' [0, 1]` and differentiable on open strip
`re ⁻¹' (0, 1)`. If, for all `z.re = 0`, `‖f z‖ ≤ a` for some `a ∈ ℝ` and, similarly, for all
`z.re = 1`, `‖f z‖ ≤ b` for some `b ∈ ℝ` then for all `z` in the closed strip
`re ⁻¹' [0, 1]` the inequality `‖f(z)‖ ≤ a ^ (1 - z.re) * b ^ z.re` holds.  -/
Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) {z : ℂ} {a b : ℝ},
  z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 →
    DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
      BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
        (∀ z ∈ Complex.re ⁻¹' {0}, ‖f z‖ ≤ a) →
          (∀ z ∈ Complex.re ⁻¹' {1}, ‖f z‖ ≤ b) → ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {Y : C} →
        (homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)) →
          autoParam
              (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
                homEquiv (CategoryTheory.CategoryStruct.comp f g) =
                  (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g))
              CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam →
            F.RepresentableBy Y
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_prod_type_right : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
  (f : α₁ × α₂ → γ), ∏ x, f x = ∏ y, ∏ x, f (x, y)
-- Mathlib.Algebra.Module.LinearMap.Defs
RingHom.toSemilinearMap_apply : ∀ {R : Type u_1} {S : Type u_5} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (a : R),
  f.toSemilinearMap a = (↑↑f).toFun a
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.instances : Lean.Meta.SynthInstance.GeneratorNode → Array Lean.Meta.SynthInstance.Instance
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- a choice of cokernel of the induced morphism `S.f' : S.X₁ ⟶ K`  -/
CategoryTheory.ShortComplex.LeftHomologyData.H : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {S : CategoryTheory.ShortComplex C} → S.LeftHomologyData → C
-- Mathlib.Order.Hom.WithTopBot
/-- A version of `Equiv.optionCongr` for `WithBot`.  -/
OrderIso.withBotCongr : {α : Type u_1} → {β : Type u_2} → [inst : PartialOrder α] → [inst_1 : PartialOrder β] → α ≃o β → WithBot α ≃o WithBot β
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.comap_comp : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} {N : Type u_3} [inst_1 : AddGroup H] [inst_2 : AddGroup N]
  (f : G →+ H) (g : H →+ N) (K : FiniteIndexNormalAddSubgroup N),
  FiniteIndexNormalAddSubgroup.comap (g.comp f) K =
    FiniteIndexNormalAddSubgroup.comap f (FiniteIndexNormalAddSubgroup.comap g K)
-- Mathlib.Algebra.BigOperators.Finprod
hasFiniteSupport_of_finsum_eq_one : ∀ {α : Type u_1} {R : Type u_7} [inst : NonAssocSemiring R] {f : α → R},
  ∑ᶠ (i : α), f i = 1 → Function.HasFiniteSupport f
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- The universe lift functor for finitely generated algebras is fully faithful.  -/
FGAlgCat.fullyFaithfulUliftFunctor : (R : Type u) → [inst : CommRing R] → (FGAlgCat.uliftFunctor R).FullyFaithful
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_comap_comap_eq_relrank_inf : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E)
  {L : Type v} [inst_3 : Field L] [inst_4 : Algebra F L] (f : L →ₐ[F] E),
  (IntermediateField.comap f A).relrank (IntermediateField.comap f B) = A.relrank (B ⊓ f.fieldRange)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformContinuous_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α], UniformContinuous TopologicalSpace.Compacts.toCloseds
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_add_of_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι),
  a ∈ s → b ∈ s → a ≠ b → (∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) → ∑ x ∈ s, f x = f a + f b
-- Mathlib.Algebra.Order.Round
sub_half_lt_round : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  x - 1 / 2 < ↑(round x)
-- Init.Data.Ord.Basic
Ordering.isGE_eq : Ordering.eq.isGE = true
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instInjectiveObjIsInjectiveXIntInjectiveObjectPlus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex.Plus (CategoryTheory.InjectiveObject C)) (n : ℤ), CategoryTheory.Injective (K.obj.X n).obj
-- Mathlib.Order.Hom.Basic
OrderHom.diag_coe : ∀ {α : Type u_2} [inst : Preorder α] (x : α), OrderHom.diag x = (x, x)
-- Init.Data.Nat.Lemmas
/-- Tail-recursive runtime replacement for `decidableExistsLT`.  -/
Nat.decidableExistsLTTR : {p : ℕ → Prop} → [DecidablePred p] → (n : ℕ) → Decidable (∃ m < n, p m)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Lean.Meta.Closure
Lean.Meta.Closure.visitExpr : (Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr) → Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation.check : {m : Type → Type u_1} → [Lean.Server.MonadCancellable m] → m Unit
-- Mathlib.Algebra.Module.Torsion.Basic
/-- can't be an instance because `hM` can't be inferred  -/
Module.IsTorsionBy.hasSMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {r : R} → Module.IsTorsionBy R M r → SMul (R ⧸ Ideal.span {r}) M
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {lo hi a : α}, (Std.PRange.succ a ∈ (Std.PRange.succ lo)...=Std.PRange.succ hi) ↔ a ∈ lo...=hi
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_minEntry_eq_minEntry? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  some (l.minEntry he) = l.minEntry?
-- Mathlib.Algebra.Group.Action.Option
Option.smul_def : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] (a : M) (x : Option α), a • x = Option.map (fun x => a • x) x
-- Batteries.Data.Array.Scan
Array.toList_scanrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → m β}
  {as : Array α}, Array.toList <$> Array.scanrM f init as = List.scanrM f init as.toList
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  ↑(Subalgebra.centralizer R s) = s.centralizer
-- Mathlib.Topology.NhdsSet
eventually_nhdsSet_iUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Sort u_4} {s : ι → Set X} {P : X → Prop},
  (∀ᶠ (x : X) in nhdsSet (⋃ i, s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in nhdsSet (s i), P x
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.parser.injEq : ∀ (catName declName : Lean.Name) (prio : ℕ) (catName_1 declName_1 : Lean.Name) (prio_1 : ℕ),
  (Lean.Parser.ParserExtension.OLeanEntry.parser catName declName prio =
      Lean.Parser.ParserExtension.OLeanEntry.parser catName_1 declName_1 prio_1) =
    (catName = catName_1 ∧ declName = declName_1 ∧ prio = prio_1)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_iff_condIndep : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ)
  (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
    ProbabilityTheory.CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic n R` is different from `0`.  -/
Polynomial.cyclotomic_ne_zero : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R] [Nontrivial R], Polynomial.cyclotomic n R ≠ 0
-- Lean.Server.AsyncList
Lean.AsyncList.cons.sizeOf_spec : ∀ {ε : Type u} {α : Type v} [inst : SizeOf ε] [inst_1 : SizeOf α] (hd : α) (tl : Lean.AsyncList ε α),
  sizeOf (Lean.AsyncList.cons hd tl) = 1 + sizeOf hd + sizeOf tl
-- Mathlib.Topology.DiscreteSubset
/-- In a T1Space, a set `s` is codiscreteWithin `U` iff it has locally finite complement within `U`.
More precisely: `s` is codiscreteWithin `U` iff every point `z ∈ U` has a punctured neighborhood
intersect `U \ s` in only finitely many points.  -/
codiscreteWithin_iff_locallyFiniteComplementWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s U : Set X},
  s ∈ Filter.codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ (U \ s)).Finite
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_fst_assoc : ∀ (X : TopCat) {Z : TopCat} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X TopCat.I) h) =
    h
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_right_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S) (b : B), (Algebra.TensorProduct.productMap f g) (1 ⊗ₜ[R] b) = g b
-- Batteries.Data.BinomialHeap.Basic
/-- The return type of `FindMin`, which encodes various quantities needed to
reconstruct the tree in `deleteMin`.
 -/
Batteries.BinomialHeap.Imp.FindMin : Type u_1 → Type u_1
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_of_subsingleton : ∀ {α : Type u_1} (a : α) [Subsingleton α], Nat.card α = 1
-- Mathlib.GroupTheory.PresentedGroup
/-- Given a set of relations, `rels`, over a type `α`, `PresentedGroup` constructs the group with
generators `x : α` and relations `rels` as a quotient of `FreeGroup α`.  -/
PresentedGroup : {α : Type u_1} → Set (FreeGroup α) → Type u_1
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.slitPlane_arg_ne_pi : ∀ {z : ℂ}, z ∈ Complex.slitPlane → z.arg ≠ Real.pi
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.optionEquivalence.match_1.splitter : {J : Type u_1} →
  (motive : Option J → Sort u_2) → (i : Option J) → (Unit → motive none) → ((i : J) → motive (some i)) → motive i
-- Plausible.Testable
Plausible.TestResult.success.injEq : ∀ {p : Prop} (a a_1 : Unit ⊕' p), (Plausible.TestResult.success a = Plausible.TestResult.success a_1) = (a = a_1)
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- A typeclass describing the property that forming the disjoint union is stable under the
property `P`.
 -/
CompHausLike.HasExplicitFiniteCoproduct : {P : TopCat → Prop} → {α : Type w} → (α → CompHausLike P) → Prop
-- Mathlib.Algebra.Quaternion
Quaternion.rank_eq_four : ∀ {R : Type u_3} [inst : CommRing R] [StrongRankCondition R], Module.rank R (Quaternion R) = 4
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_of_injective_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (α : CochainComplex.HomComplex.Cochain K L (-1)) (n m : ℤ),
  n + 1 = m →
    HomologicalComplex.ExactAt K m →
      ∀ [CategoryTheory.Injective (L.X m)],
        (CochainComplex.HomComplex.δ (-1) 0 α).EqUpTo (CochainComplex.HomComplex.Cochain.ofHom f) n →
          ∃ h,
            (CochainComplex.HomComplex.δ (-1) 0 (α + CochainComplex.HomComplex.Cochain.single h (-1))).EqUpTo
              (CochainComplex.HomComplex.Cochain.ofHom f) m
-- Mathlib.GroupTheory.PGroup
IsPGroup.powEquiv_symm_apply : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) (g : G),
  (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingDegree ≠ 0 ↔ p.coeff 0 = 0
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.open_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (self : Bundle.Pretrivialization F proj), IsOpen self.baseSet
-- Init.Data.BitVec.Lemmas
BitVec.mul_eq_and : ∀ {a b : BitVec 1}, a * b = a &&& b
-- Mathlib.Order.Basic
Decidable.ne_iff_gt_iff_ge : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableEq α], (a ≠ b ↔ b < a) ↔ b ≤ a
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A copy of `Finsupp.distribMulActionHom_ext'` for `MonoidAlgebra`.  -/
MonoidAlgebra.distribMulActionHom_ext' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] {N : Type u_7} [inst_1 : Monoid R]
  [inst_2 : AddMonoid N] [inst_3 : DistribMulAction R N] [inst_4 : DistribMulAction R S]
  {f g : MonoidAlgebra S M →+[R] N},
  (∀ (a : M), f.comp (MonoidAlgebra.singleDistribMulActionHom a) = g.comp (MonoidAlgebra.singleDistribMulActionHom a)) →
    f = g
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.neg_right : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α : u ⟶ v), CategoryTheory.Arrow.Hom.right (-α) = -CategoryTheory.Arrow.Hom.right α
-- Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Algebra.isIntegral_iff : ∀ (R : Type u_1) (A : Type u_3) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x
-- Mathlib.Topology.Constructions.SumProd
/-- `Prod.fst` maps neighborhood of `x : X × Y` within the section `Prod.snd ⁻¹' {x.2}`
to `𝓝 x.1`.  -/
map_fst_nhdsWithin : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
  Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1