mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_aleph0_iff : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J],
  CategoryTheory.IsCardinalFiltered J Cardinal.aleph0 ↔ CategoryTheory.IsFiltered J
-- Mathlib.Data.Sym.Basic
Sym.fill.eq_1 : ∀ {α : Type u_1} {n : ℕ} (a : α) (i : Fin (n + 1)) (m : Sym α (n - ↑i)),
  Sym.fill a i m = (Sym.cast ⋯) (m.append (Sym.replicate (↑i) a))
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.comp_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g : B ⟶ C)
  (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Lean.Data.NameTrie
Lean.NameTrie.matchingToArray : {β : Type u_1} → Lean.NameTrie β → Lean.Name → Array β
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.isSeparable : ∀ (K : Type u_1) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [Algebra.FormallyUnramified K L] [Algebra.EssFiniteType K L], Algebra.IsSeparable K L
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.mem_periodicPts_iff_isPeriodicPt_factorial_card : ∀ {α : Type u_1} {f : α → α} {x : α} [inst : Fintype α],
  x ∈ Function.periodicPts f ↔ Function.IsPeriodicPt f (Fintype.card α).factorial x
-- Mathlib.Topology.Connected.PathConnected
Inseparable.joinedIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, Inseparable x y → x ∈ F → y ∈ F → JoinedIn F x y
-- Lean.ReducibilityAttrs
/-- Return the reducibility attribute for the given declaration.  -/
Lean.getReducibilityStatus : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Lean.ReducibilityStatus
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_compl_iff : ∀ {α : Type u_1} [inst : LE α] {s : LowerSet α} {a : α}, a ∈ s.compl ↔ a ∉ s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {p : α → Prop}, m.WF → ((∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h))
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.injOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Set.InjOn (↑e) e.source
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₂ : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.hom.app X).hom₂ = CategoryTheory.CategoryStruct.id (F.obj X.obj₃)
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.isUnit_iff_ker_eq_bot : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (f : V →ₗ[K] V), IsUnit f ↔ f.ker = ⊥
-- Std.Data.DTreeMap.Basic
/-- Transforms an array of mappings into a tree map.  -/
Std.DTreeMap.ofArray : {α : Type u} →
  {β : α → Type v} →
    Array ((a : α) × β a) → (cmp : autoParam (α → α → Ordering) Std.DTreeMap.ofArray._auto_1) → Std.DTreeMap α β cmp
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Useful to use together with `Continuous.comp₂`.  -/
IsBoundedBilinearMap.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G}, IsBoundedBilinearMap 𝕜 f → Continuous f
-- Mathlib.Data.Set.Card
Set.one_lt_ncard_iff_nontrivial_and_finite : ∀ {α : Type u_1} {s : Set α}, 1 < s.ncard ↔ s.Nontrivial ∧ s.Finite
-- Mathlib.Order.SuccPred.Basic
Order.pred_top_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α} [inst_2 : OrderTop α],
  Order.pred ⊤ ≤ a ↔ a = ⊤ ∨ a = Order.pred ⊤
-- Mathlib.Algebra.Divisibility.Prod
Prod.mk_dvd_mk : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Semigroup G₁] [inst_1 : Semigroup G₂] {x₁ y₁ : G₁} {x₂ y₂ : G₂},
  (x₁, x₂) ∣ (y₁, y₂) ↔ x₁ ∣ y₁ ∧ x₂ ∣ y₂
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- For `n` positive, the number of principal ideals in `𝓞 K` of norm `n` multiplied by the order
of the torsion of `K` is equal to the number of elements in `integerSet K` of norm `n`.  -/
NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (n : ℕ),
  Nat.card ↑{I | Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n} * NumberField.Units.torsionOrder K =
    Nat.card ↑{a | NumberField.mixedEmbedding.norm ↑a = ↑n}
-- Mathlib.Data.Finset.Insert
Finset.singleton_val : ∀ {α : Type u_1} (a : α), {a}.val = {a}
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.val : Lean.Elab.FieldInfo → Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {fallback : α}, l.isEmpty = true → Std.Internal.List.minKeyD l fallback = fallback
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.mulRight.eq_1 : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.mulRight a = (toUnits a).mulRight
-- Mathlib.Data.Set.Finite.Basic
Set.exists_finite_iff_finset : ∀ {α : Type u} {p : Set α → Prop}, (∃ s, s.Finite ∧ p s) ↔ ∃ s, p ↑s
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that members of `sInfHomClass`s commute with arbitrary infima/meets.  -/
sInfHomClass.map_sInf : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {inst : InfSet α} {inst_1 : InfSet β} {inst_2 : FunLike F α β}
  [self : sInfHomClass F α β] (f : F) (s : Set α), f (sInf s) = sInf (⇑f '' s)
-- Mathlib.MeasureTheory.Function.EssSup
essSup_mono_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] {f g : α → β},
  f ≤ᵐ[μ] g →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) essSup_mono_ae._auto_1 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) g) essSup_mono_ae._auto_3 →
        essSup f μ ≤ essSup g μ
-- Init.Data.String.Basic
String.Slice.utf8ByteSize_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceFrom pos).utf8ByteSize = s.utf8ByteSize - pos.offset.byteIdx
-- Mathlib.Algebra.Free
FreeAddMagma.instInhabited.eq_1 : ∀ {α : Type u} [inst : Inhabited α], FreeAddMagma.instInhabited = { default := FreeAddMagma.of default }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w n : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc =
    if curr < n - 1 then
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.twoPowShift aig
          { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
      let aig_1 := res.aig;
      have acc_1 := res.vec;
      have this := ⋯;
      have distance := distance.cast this;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig_1 distance (curr + 1) acc_1
    else { aig := aig, vec := acc }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastConst : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (c : BitVec w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign, { aig := aig, ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig c).get idx hidx }⟧ = c.getLsbD idx
-- Mathlib.LinearAlgebra.Complex.Module
Complex.selfAdjointEquiv_symm_apply : ∀ (x : ℝ), Complex.selfAdjointEquiv.symm x = ⟨↑x, ⋯⟩
-- Init.Data.Array.Lemmas
Array.filter_push : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α},
  Array.filter p (xs.push a) = if p a = true then (Array.filter p xs).push a else Array.filter p xs
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.ProofInstInfo.mk.inj : ∀ {argsInfo argsInfo_1 : Array Lean.Meta.Sym.ProofInstArgInfo},
  { argsInfo := argsInfo } = { argsInfo := argsInfo_1 } → argsInfo = argsInfo_1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.self_comp_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), ⇑e ∘ ⇑e.symm = id
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {km : α}, t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRangeₐ_mk : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) {d : RingCon N} (h : d = c.comap f)
  (x : N), (c.comapQuotientEquivRangeₐ f h) ↑x = ⟨↑(f x), ⋯⟩
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Dynamics.Flow
Flow.mem_orbit_of_mem_orbit : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  (ϕ : Flow τ α) {x₁ x₂ : α} (t : τ), x₂ ∈ ϕ.orbit x₁ → ϕ.toFun t x₂ ∈ ϕ.orbit x₁
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- ...factorizing the components of `e` through the components of `π`...  -/
CategoryTheory.EffectiveEpiFamilyStruct.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} (self : CategoryTheory.EffectiveEpiFamilyStruct X π) {W : C} (e : (a : α) → X a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
  (a : α), CategoryTheory.CategoryStruct.comp (π a) (self.desc e ⋯) = e a
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) {x : M}, x ∈ ↑N ↔ x ∈ N
-- Mathlib.Algebra.Homology.HomologySequence
/-- If `c.Rel i j` and `Hᵢ(X₂), Hⱼ(X₂)` are trivial, `δ` defines an isomorphism
`Hᵢ(X₃) ≅ Hⱼ(X₁)`.  -/
CategoryTheory.ShortComplex.ShortExact.δIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            S.ShortExact →
              (i j : ι) →
                c.Rel i j →
                  CategoryTheory.Limits.IsZero (S.X₂.homology i) →
                    CategoryTheory.Limits.IsZero (S.X₂.homology j) → (S.X₃.homology i ≅ S.X₁.homology j)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.nonneg_neg_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_nonneg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.Algebra.Group.Prod
MonoidHom.fst_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N) (g : M →* P), (MonoidHom.fst N P).comp (f.prod g) = f
-- Mathlib.Topology.Algebra.ConstMulAction
interior_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] (c : G) (s : Set α), interior (c +ᵥ s) = c +ᵥ interior s
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.apply_zero : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) (x : X), F (0, x) = f₀ x
-- Aesop.Forward.Match.Types
Aesop.Match.mk.injEq : ∀ (subst : Aesop.Substitution) (patInstSubsts : Array Aesop.Substitution) (level : Aesop.SlotIndex)
  (forwardDeps conclusionDeps : Array Aesop.PremiseIndex) (subst_1 : Aesop.Substitution)
  (patInstSubsts_1 : Array Aesop.Substitution) (level_1 : Aesop.SlotIndex)
  (forwardDeps_1 conclusionDeps_1 : Array Aesop.PremiseIndex),
  ({ subst := subst, patInstSubsts := patInstSubsts, level := level, forwardDeps := forwardDeps,
        conclusionDeps := conclusionDeps } =
      { subst := subst_1, patInstSubsts := patInstSubsts_1, level := level_1, forwardDeps := forwardDeps_1,
        conclusionDeps := conclusionDeps_1 }) =
    (subst = subst_1 ∧
      patInstSubsts = patInstSubsts_1 ∧
        level = level_1 ∧ forwardDeps = forwardDeps_1 ∧ conclusionDeps = conclusionDeps_1)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.linearEquivOfRightInverse_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Invertible R M] [inst_6 : Module.Invertible R N]
  {f : M →ₗ[R] N} {g : N →ₗ[R] M} (hfg : Function.RightInverse ⇑f ⇑g) (x : M),
  (Module.Invertible.linearEquivOfRightInverse hfg) x = f x
-- Batteries.Data.HashMap.Basic
/-- Runs a monadic function over the elements in the map (in arbitrary order).
```
def checkEven (k : String) (v : Nat) : Except String Unit :=
  if v % 2 == 0 then pure () else throw s!"value {v} at key {k} is not even"

forM checkEven (ofList [("one", 1), ("three", 3)]) = Except.error "value 3 at key three is not even"
forM checkEven (ofList [("two", 2), ("four", 4)]) = Except.ok ()
```
 -/
Batteries.HashMap.forM : {α : Type u_1} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {m : Type u_2 → Type u_3} →
        {β : Type u_4} → [Monad m] → (α → β → m PUnit.{u_2 + 1}) → Batteries.HashMap α β → m PUnit.{u_2 + 1}
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_fst_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q)
  {Z : C} (h : K.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.fst φ).f q) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `toUpperSet` as an `OrderIso`  -/
Topology.WithUpperSet.toUpperSetOrderIso : {α : Type u_1} → [inst : Preorder α] → α ≃o Topology.WithUpperSet α
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- The indicator of a set $A$ and a random variable $X$ are independent
if for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$  -/
indicator_indepFun_of_bcf : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {G : Type u_6} [inst : TopologicalSpace G]
  [inst_1 : MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G] {Z : Ω → G}
  [MeasureTheory.IsProbabilityMeasure P] {A : Set Ω},
  MeasureTheory.NullMeasurableSet A P →
    AEMeasurable Z P →
      (∀ (f : BoundedContinuousFunction G ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P) →
        ProbabilityTheory.IndepFun (A.indicator 1) Z P
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- If `f, g` is an `F`-cosplit pair, then `F` creates limits of `parallelPair f g`.  -/
CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair.out : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₁, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F] →
            {A B : C} →
              (f g : A ⟶ B) →
                [F.IsCosplitPair f g] → CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.Combinatorics.Optimization.ValuedCSP
FractionalOperation.size.eq_1 : ∀ {D : Type u_1} {m : ℕ} (ω : FractionalOperation D m), ω.size = Multiset.card ω
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The canonical diffeomorphism `(M ⊕ N) ⊕ P → M ⊕ (N ⊕ P)`  -/
Diffeomorph.sumAssoc : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_5} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                (M : Type u_9) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (n : WithTop ℕ∞) →
                        (M' : Type u_13) →
                          [inst_6 : TopologicalSpace M'] →
                            [inst_7 : ChartedSpace H M'] →
                              (M'' : Type u_14) →
                                [inst_8 : TopologicalSpace M''] →
                                  [inst_9 : ChartedSpace H M''] → Diffeomorph I I ((M ⊕ M') ⊕ M'') (M ⊕ M' ⊕ M'') n
-- Mathlib.Topology.Neighborhoods
eventually_eventually_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {p : X → Prop},
  (∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhds x, p x
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_id : ∀ {P : Type u_3} [inst : Add P] (S : AddSubsemigroup P), AddSubsemigroup.comap (AddHom.id P) S = S
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj : ∀ (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ),
  CategoryTheory.Limits.walkingSpanOpEquiv.functor.obj X = Opposite.unop X
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
_private.Mathlib.MeasureTheory.Function.SimpleFuncDense.0.MeasureTheory.SimpleFunc.nearestPtInd.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((N : ℕ) → motive N.succ) → motive x
-- Lean.Elab.Syntax
/-- Auxiliary function for creating declaration names from parser descriptions.
Example:
Given
```
syntax term "+" term : term
syntax "[" sepBy(term, ", ") "]"  : term
```
It generates the names `term_+_` and `term[_,]`
 -/
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.mkNameFromParserSyntax : Lean.Name → Lean.Syntax → Lean.MacroM Lean.Name
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_natCast_ite : ∀ {R : Type u} {m n : ℕ} [inst : Semiring R], (↑m).coeff n = ↑(if n = 0 then m else 0)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp] [Std.TransCmp cmp]
  {k : α}, t.toArray.contains k = t.contains k
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPForalls : Lean.Options → Bool
-- Mathlib.RingTheory.RamificationInertia.Inertia
Localization.AtPrime.algebraOfLiesOver.congr_simp : ∀ {A : Type u_4} {B : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] (p : Ideal A)
  [inst_3 : p.IsPrime] (P : Ideal B) [inst_4 : P.IsPrime] [inst_5 : P.LiesOver p],
  Localization.AtPrime.algebraOfLiesOver p P = Localization.AtPrime.algebraOfLiesOver p P
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F), (H.mapCone c).pt = H.obj c.pt
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_lt_top : ∀ {r : ENNReal}, ⌈r⌉ₑ < ⊤ ↔ r < ⊤
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.odd_card_of_involutive : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → Odd (Nat.card G)
-- Mathlib.Algebra.Order.Kleene
one_add_mul_kstar : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a : α}, 1 + a * KStar.kstar a = KStar.kstar a
-- Init.Data.Array.Lemmas
Array.allM_eq_not_anyM_not : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α},
  Array.allM p as = (fun x => !x) <$> Array.anyM (fun x => (fun x => !x) <$> p x) as
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.elab : Lean.Elab.Term.SavedState → Lean.Elab.Term.State
-- Mathlib.Order.Closure
ClosureOperator.toOrderHom : {α : Type u_1} → [inst : Preorder α] → ClosureOperator α → α →o α
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict'_id : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} (B : Type u_6) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : Algebra K L]
  [inst_7 : Algebra A L] [inst_8 : IsScalarTower A K L] [inst_9 : Algebra B L] [inst_10 : IsScalarTower A B L]
  [inst_11 : IsIntegralClosure B A L], galRestrict' A B B (AlgHom.id K L) = AlgHom.id A B
-- Mathlib.Topology.Category.TopCat.Basic
/-- The category of topological spaces.  -/
TopCat : Type (u + 1)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.inv_natCast_cpow_ofReal_pos : ∀ {n : ℕ}, n ≠ 0 → ∀ (x : ℝ), 0 < (↑n ^ ↑x)⁻¹
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.ext_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : PartialHomeomorph X Y},
  e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
/-- The cardinal of the set of linearly independent vectors over a finite-dimensional vector space
over a finite field.  -/
card_linearIndependent : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : Fintype K] [Finite V] {k : ℕ},
  k ≤ Module.finrank K V →
    Nat.card { s // LinearIndependent K s } = ∏ i, (Fintype.card K ^ Module.finrank K V - Fintype.card K ^ ↑i)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.top : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, ⊤.IsQF
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_iInter_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (s : Set α) (t : ι → Set β),
  s +ᵥ ⋂ i, t i ⊆ ⋂ i, s +ᵥ t i
-- Init.Data.String.Basic
String.Pos.offset_next : ∀ {s : String} (p : s.Pos) (h : p ≠ s.endPos), (p.next h).offset = p.offset + p.get h
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State : Type
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.ext_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂}, f = g ↔ ∀ (x : E), f x = g x
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_conj : ∀ (x : ℂ), Complex.tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.tanh x)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X Y : C}
  (f : X ⟶ Y) (T : Type wᵒᵖ), (CategoryTheory.Limits.piFunctor.map f).app T = CategoryTheory.Limits.Pi.map fun x => f